diff options
| author | Akshay Nair <phenax5@gmail.com> | 2023-12-16 17:31:12 +0530 |
|---|---|---|
| committer | Akshay Nair <phenax5@gmail.com> | 2023-12-16 17:36:36 +0530 |
| commit | 4a0fb237cac8796e45d7b217db0d808452454820 (patch) | |
| tree | 6ae2177bd6f75d5e589adf3edccc31842a10b99c /src/utils/theorem.ts | |
| parent | efc0358c1e2b52308d3df68aa713cef5dc6e6bfe (diff) | |
| download | ts-theorem-provinator-4a0fb237cac8796e45d7b217db0d808452454820.tar.gz ts-theorem-provinator-4a0fb237cac8796e45d7b217db0d808452454820.zip | |
feat: lambda calculus
Diffstat (limited to 'src/utils/theorem.ts')
| -rw-r--r-- | src/utils/theorem.ts | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/src/utils/theorem.ts b/src/utils/theorem.ts index a4dd2e9..be19b94 100644 --- a/src/utils/theorem.ts +++ b/src/utils/theorem.ts @@ -6,9 +6,9 @@ export type OpToStr<O extends Op> = O extends string ? O : O extends { op: string, a: infer a extends string, b: infer b extends string } ? `(${a} ${O['op']} ${b})` - : O extends { op: string, a: infer a extends DyadicOp, b: infer b extends string } ? `(${OpToStr<a>} ${O['op']} ${b})` - : O extends { op: string, a: infer a extends string, b: infer b extends DyadicOp } ? `(${a} ${O['op']} ${OpToStr<b>})` - : O extends { op: string, a: infer a extends DyadicOp, b: infer b extends DyadicOp } ? `(${OpToStr<a>} ${O['op']} ${OpToStr<b>})` + : O extends { op: string, a: infer a extends DyadicOp | MonadicOp, b: infer b extends string } ? `(${OpToStr<a>} ${O['op']} ${b})` + : O extends { op: string, a: infer a extends string, b: infer b extends DyadicOp | MonadicOp } ? `(${a} ${O['op']} ${OpToStr<b>})` + : O extends { op: string, a: infer a extends DyadicOp | MonadicOp, b: infer b extends DyadicOp | MonadicOp } ? `(${OpToStr<a>} ${O['op']} ${OpToStr<b>})` : O extends { op: string, a: infer a extends string } ? `${O['op']}(${a})` : O extends { op: string, a: infer a extends DyadicOp } ? `${O['op']}(${OpToStr<a>})` : never; @@ -30,6 +30,7 @@ export interface Rewrite<left extends Op, right extends Op, Typ extends RwType = export type Sym<R extends RewriteBase> = Rewrite<R['right'], R['left'], R['type']>; export type Subst<A extends Op, B extends Op> = Rewrite<A, B> +export type SubstEq<O extends Equation<Op, Op>> = Rewrite<O['a'], O['b']> export type ApplyRewrite<O extends Op, R extends RewriteBase> = R['type'] extends 'imperative' ? (R & { left: O })['right'] |