diff options
Diffstat (limited to 'src/index.ts')
| -rw-r--r-- | src/index.ts | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/src/index.ts b/src/index.ts index 276bbe9..4a00438 100644 --- a/src/index.ts +++ b/src/index.ts @@ -1,5 +1,5 @@ import { Add, Multiply, Succ, _0, _1, _3 } from './nat'; -import { Op, Rewrite, ChainRewrites, Sym, Equation, Refl, VerifyEquation, assert, RewriteBase, Subst, ApplyRewrite, Evaluate, ReflR, OpToStr } from './util'; +import { Op, Rewrite, ChainRewrites, Sym, Equation, Refl, VerifyEquation, assert, Subst, ApplyRewrite, Evaluate, OpToStr } from './util'; export namespace addition { // Identity @@ -186,7 +186,7 @@ export namespace multiplication { } export namespace equation { - type F<X extends Op> = { op: '<F>', a: _0, b: X }; + type F<X extends Op> = { op: 'F', a: X }; export type Reflexivity<A extends Op> = Rewrite<Equation<A, A>, 'true'>; @@ -194,7 +194,7 @@ export namespace equation { export type Congruence<A extends Op, B extends Op> = Rewrite<Equation<A, B>, Equation<F<A>, F<B>>>; - export type SubstituteEq<O extends { op: '=', a: Op, b: Op }> = Rewrite<O['a'], O['b']> + export type SubstituteEq<O extends Equation<Op, Op>> = Rewrite<O['a'], O['b']> export interface SubstituteEq_Proof<A extends Op, B extends Op> { type: 'rewrite', known: { |