From a393765df40744aae68dab943e25bad8175bd5c0 Mon Sep 17 00:00:00 2001
From: Akshay Nair <phenax5@gmail.com>
Date: Tue, 12 Dec 2023 20:21:13 +0530
Subject: feat: associativity + distributivity for multiplication

---
 src/tests.ts | 14 +++++++++++++-
 1 file changed, 13 insertions(+), 1 deletion(-)

(limited to 'src/tests.ts')

diff --git a/src/tests.ts b/src/tests.ts
index 5c066dc..04a009a 100644
--- a/src/tests.ts
+++ b/src/tests.ts
@@ -1,6 +1,6 @@
 import { addition, multiplication } from './index';
 import { Add, Multiply, Succ } from './nat';
-import { ApplyRewrite, ChainRewrites, Flip, Eq, VerifyEquation, Equation, assert } from './util';
+import { ApplyRewrite, ChainRewrites, Flip, Eq, VerifyEquation, Equation, assert, Evaluate } from './util';
 
 export type specChainRewrites = [
   assert<Eq<
@@ -70,4 +70,16 @@ export namespace multiplication_spec {
       Multiply<Multiply<'B', 'A'>, 'C'>
     >>,
   ]
+  export type specDistributivity = [
+    assert<Eq<
+      Evaluate<multiplication.Distributivity<'A', 'B', 'C'>>,
+      Add<Multiply<'A', 'C'>, Multiply<'B', 'C'>>
+    >>,
+  ]
+  export type specAssociativity = [
+    assert<Eq<
+      Evaluate<multiplication.Associativity<'A', 'B', 'C'>>,
+      Multiply<'A', Multiply<'B', 'C'>>
+    >>,
+  ]
 }
-- 
cgit v1.3.1