feat: associativity and commutativity for addition

1 files changed, 16 insertions, 8 deletions

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'>;