diff options
| author | Akshay Nair <phenax5@gmail.com> | 2023-12-10 16:15:00 +0530 |
|---|---|---|
| committer | Akshay Nair <phenax5@gmail.com> | 2023-12-10 16:32:23 +0530 |
| commit | f6e26212620de411e082cbd52379075ea5a99032 (patch) | |
| tree | a7a68c681a3e99987f2bb02eebf51616f6a65067 /src/index.ts | |
| download | ts-theorem-provinator-f6e26212620de411e082cbd52379075ea5a99032.tar.gz ts-theorem-provinator-f6e26212620de411e082cbd52379075ea5a99032.zip | |
init commit rewriting shit
Diffstat (limited to '')
| -rw-r--r-- | src/index.ts | 43 |
1 files changed, 43 insertions, 0 deletions
diff --git a/src/index.ts b/src/index.ts new file mode 100644 index 0000000..bd93300 --- /dev/null +++ b/src/index.ts @@ -0,0 +1,43 @@ +export type Op = string | { op: string; a: Op; b: Op }; + +export type Rewrite<left extends Op, right extends Op> = { + type: 'rewrite'; + left: left; + right: right; +}; +export type RewriteKind = Rewrite<Op, Op>; + +export type Flip<R extends RewriteKind> = Rewrite<R['right'], R['left']>; + +export type ApplyRewrite<O extends Op, R extends RewriteKind> = + O extends R['left'] ? R['right'] + : 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> } + : Omit<O, 'a'> & { a: ApplyRewrite<O['a'], R> } + ) + : never; + +export type Add<a extends Op, b extends Op> = { op: '+'; a: a; b: b }; + +export type Identity<A extends Op> = Rewrite<Add<A, '0'>, A>; +export type Commutativity<A extends Op, B extends Op> = Rewrite<Add<A, B>, Add<B, A>>; + +// type _x = ApplyRewrite<Add<'A', '1'>, Identity<'0'>>; + +// type Assoc<A extends Op, B extends Op> = + +/* + +Assoc: (a + b) + c = a + (b + c) + +For a = 0, +(0 + b) + c += b + c += 0 + (b + c) + +For a = succ(), + +*/ + |
