From 4a0fb237cac8796e45d7b217db0d808452454820 Mon Sep 17 00:00:00 2001
From: Akshay Nair <phenax5@gmail.com>
Date: Sat, 16 Dec 2023 17:31:12 +0530
Subject: feat: lambda calculus

---
 src/equation.ts | 9 ++++-----
 1 file changed, 4 insertions(+), 5 deletions(-)

(limited to 'src/equation.ts')

diff --git a/src/equation.ts b/src/equation.ts
index 0ec25d6..cc668b1 100644
--- a/src/equation.ts
+++ b/src/equation.ts
@@ -1,4 +1,4 @@
-import { Op, Rewrite, ChainRewrites, Sym, Equation, VerifyEquation, assert, ApplyRewrite, Evaluate, OpToStr } from './utils/theorem';
+import { Op, Rewrite, ChainRewrites, Sym, Equation, VerifyEquation, assert, ApplyRewrite, Evaluate, OpToStr, SubstEq } from './utils/theorem';
 
 export namespace equation {
   type F<X extends Op> = { op: 'F', a: X };
@@ -9,7 +9,6 @@ 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 Equation<Op, Op>> = Rewrite<O['a'], O['b']>
   export interface SubstituteEq_Proof<A extends Op, B extends Op> {
     type: 'rewrite',
     known: {
@@ -18,7 +17,7 @@ export namespace equation {
     left: Equation<F<A>, F<B>>; // f(a) = f(b)
     right: ChainRewrites<[
       Sym<Congruence<A, B>>,                   // a = b
-      SubstituteEq<this['known']['a = b']>,    // b = b
+      SubstEq<this['known']['a = b']>,         // b = b
       Reflexivity<B>,
     ], this['left']>;
   };
@@ -36,8 +35,8 @@ export namespace equation {
     },
     left: Equation<Equation<A, B>, Equation<B, C>>; // (a = b) = (b = c)
     right: ChainRewrites<[
-      SubstituteEq<this['known']['a = b']>,                                 // (b = b) = (b = c)
-      SubstituteEq<ApplyRewrite<this['known']['b = c'], Symmetry<B, C>>>,   // (b = b) = (c = b)
+      SubstEq<this['known']['a = b']>,                                 // (b = b) = (b = c)
+      SubstEq<ApplyRewrite<this['known']['b = c'], Symmetry<B, C>>>,   // (b = b) = (c = b)
       Reflexivity<B>,                                                       // true = (b = b)
       Reflexivity<B>,                                                       // true = true
       Reflexivity<'true'>,
-- 
cgit v1.3.1