From efc0358c1e2b52308d3df68aa713cef5dc6e6bfe Mon Sep 17 00:00:00 2001
From: Akshay Nair <phenax5@gmail.com>
Date: Fri, 15 Dec 2023 22:36:03 +0530
Subject: refactor: moves stuff around

---
 src/tests/nat.spec.ts | 60 +++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 60 insertions(+)
 create mode 100644 src/tests/nat.spec.ts

(limited to 'src/tests/nat.spec.ts')

diff --git a/src/tests/nat.spec.ts b/src/tests/nat.spec.ts
new file mode 100644
index 0000000..acade6f
--- /dev/null
+++ b/src/tests/nat.spec.ts
@@ -0,0 +1,60 @@
+import { addition, multiplication } from '../natural-numbers';
+import { Add, Multiply, _0 } from '../utils/nat';
+import { ApplyRewrite, Sym, Eq, VerifyEquation, Equation, assert, Evaluate } from '../utils/theorem';
+
+export namespace spec_addition {
+  export type specIdentity = [
+    assert<Eq<
+      ApplyRewrite<Add<'A', Add<'B', _0>>, addition.Identity<'B'>>,
+      Add<'A', 'B'>
+    >>,
+    assert<Eq<
+      ApplyRewrite<Add<Add<'A', 'B'>, _0>, addition.Identity<Add<'A', 'B'>>>,
+      Add<'A', 'B'>
+    >>,
+    assert<Eq<
+      ApplyRewrite<Add<'A', 'B'>, Sym<addition.Identity<Add<'A', 'B'>>>>,
+      Add<Add<'A', 'B'>, _0>
+    >>,
+    assert<Eq<
+      ApplyRewrite<Add<'A', Add<'B', Add<'C', _0>>>, addition.Identity<'C'>>,
+      Add<'A', Add<'B', 'C'>>
+    >>,
+  ]
+
+  export type specCommutativity = [
+    assert<Eq<
+      ApplyRewrite<Add<'A', 'B'>, addition.Commutativity<'A', 'B'>>,
+      Add<'B', 'A'>
+    >>,
+    assert<Eq<
+      ApplyRewrite<Add<Add<'A', 'B'>, 'C'>, addition.Commutativity<'A', 'B'>>,
+      Add<Add<'B', 'A'>, 'C'>
+    >>,
+    assert<Eq<
+      ApplyRewrite<Add<'A', Add<'B', 'C'>>, addition.Commutativity<'B', 'C'>>,
+      Add<'A', Add<'C', 'B'>>
+    >>,
+  ]
+}
+
+export namespace multiplication_spec {
+  export type specCommutativity = [
+    assert<Eq<
+      ApplyRewrite<Multiply<Multiply<'A', 'B'>, 'C'>, multiplication.Commutativity<'A', 'B'>>,
+      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