feat: associativity + distributivity for multiplication

1 files changed, 13 insertions, 1 deletions

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'>>
+    >>,
+  ]
 }