From ade99f3f1fc2da1d51a82f1376c61ad609d60ff1 Mon Sep 17 00:00:00 2001
From: Akshay Nair <phenax5@gmail.com>
Date: Tue, 12 Dec 2023 17:58:46 +0530
Subject: feat: associativity and commutativity for addition

---
 src/util.ts | 24 ++++++++++++++++--------
 1 file changed, 16 insertions(+), 8 deletions(-)

(limited to 'src/util.ts')

diff --git a/src/util.ts b/src/util.ts
index 5556f70..f6067ae 100644
--- a/src/util.ts
+++ b/src/util.ts
@@ -18,14 +18,22 @@ export type ApplyRewrite<O extends Op, R extends Rewrite<Op, Op>> =
   )
   : never;
 
-// interface Kind<V = unknown> {
-//   _: V;
-//   return: unknown;
-// }
-// type Ap<K extends Kind, V> = (K & { _: V })['return'];
+export interface Kind<V = unknown, R = unknown> {
+  _: V;
+  return: R;
+}
+export type Ap<K extends Kind, V> = (K & { _: V })['return'];
 
 export type ChainRewrites<Rws extends Rewrite<Op, Op>[], O extends Op> =
   Rws extends [] ? O
-   : Rws extends [infer R extends Rewrite<Op, Op>, ...infer Rs extends Rewrite<Op, Op>[]]
-   ? ChainRewrites<Rs, ApplyRewrite<O, R>>
-   : never;
+  : Rws extends [infer R extends Rewrite<Op, Op>, ...infer Rs extends Rewrite<Op, Op>[]]
+  ? ChainRewrites<Rs, ApplyRewrite<O, R>>
+  : never;
+
+export type VerifyEquation<Eq extends Rewrite<Op, Op>> =
+  Eq['right'] extends 'true' ? true : false & Eq['right'];
+
+export type Eq<a, b> = ([a] extends [b] ? ([b] extends [a] ? true : false & { lhs: a; rhs: b }) : false & { lhs: a; rhs: b });
+
+export type Equation<A extends Op, B extends Op> = { op: '=', a: A, b: B };
+export type Refl<A extends Op> = Rewrite<Equation<A, A>, 'true'>;
-- 
cgit v1.3.1