From 3d91b8c0fe73d24e3bcf13e7d7e8079f58975500 Mon Sep 17 00:00:00 2001
From: Akshay Nair <phenax5@gmail.com>
Date: Fri, 15 Dec 2023 22:28:31 +0530
Subject: feat: adds monadic/dyadic operators

---
 src/index.ts | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'src/index.ts')

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: {
-- 
cgit v1.3.1