diff options
| author | Akshay Nair <phenax5@gmail.com> | 2023-12-12 18:47:06 +0530 |
|---|---|---|
| committer | Akshay Nair <phenax5@gmail.com> | 2023-12-12 18:47:06 +0530 |
| commit | 999c2314c0d649646a53e7cc440ae3f4aa1a3d61 (patch) | |
| tree | d475be6c55343b5ccc05d2d014897708182789cd /src/util.ts | |
| parent | ade99f3f1fc2da1d51a82f1376c61ad609d60ff1 (diff) | |
| download | ts-theorem-provinator-999c2314c0d649646a53e7cc440ae3f4aa1a3d61.tar.gz ts-theorem-provinator-999c2314c0d649646a53e7cc440ae3f4aa1a3d61.zip | |
feat: commutativity + identity for multiplication
Diffstat (limited to 'src/util.ts')
| -rw-r--r-- | src/util.ts | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/src/util.ts b/src/util.ts index f6067ae..97e9335 100644 --- a/src/util.ts +++ b/src/util.ts @@ -13,7 +13,8 @@ export type ApplyRewrite<O extends Op, R extends Rewrite<Op, Op>> = : O extends string ? O : O extends { a: Op, b: Op, op: string } ? ( ApplyRewrite<O['a'], R> extends O['a'] - ? Omit<O, 'b'> & { b: ApplyRewrite<O['b'], R> } + ? (ApplyRewrite<O['b'], R> extends O['b'] ? O + : Omit<O, 'b'> & { b: ApplyRewrite<O['b'], R> }) : Omit<O, 'a'> & { a: ApplyRewrite<O['a'], R> } ) : never; @@ -33,6 +34,7 @@ export type ChainRewrites<Rws extends Rewrite<Op, Op>[], O extends Op> = export type VerifyEquation<Eq extends Rewrite<Op, Op>> = Eq['right'] extends 'true' ? true : false & Eq['right']; +export type assert<T extends true> = T; export type Eq<a, b> = ([a] extends [b] ? ([b] extends [a] ? true : false & { lhs: a; rhs: b }) : false & { lhs: a; rhs: b }); export type Equation<A extends Op, B extends Op> = { op: '=', a: A, b: B }; |