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/theorem.spec.ts | 28 ++++++++++++++++++++++++++++
 1 file changed, 28 insertions(+)
 create mode 100644 src/tests/theorem.spec.ts

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

diff --git a/src/tests/theorem.spec.ts b/src/tests/theorem.spec.ts
new file mode 100644
index 0000000..4ab220a
--- /dev/null
+++ b/src/tests/theorem.spec.ts
@@ -0,0 +1,28 @@
+import { addition } from '../natural-numbers';
+import { Add, _0 } from '../utils/nat';
+import { ApplyRewrite, ChainRewrites, Sym, Eq, VerifyEquation, Equation, assert, Evaluate } from '../utils/theorem';
+
+export type specChainRewrites = [
+  assert<Eq<
+    ChainRewrites<
+      [
+        addition.Commutativity<_0, 'B'>,
+        addition.Identity<'B'>,
+      ],
+      Add<Add<_0, 'B'>, 'C'>
+    >,
+    Add<'B', 'C'>
+  >>,
+  assert<Eq<
+    ChainRewrites<
+      [
+        addition.Commutativity<_0, 'B'>,
+        addition.Identity<'B'>,
+        Sym<addition.Identity<Add<'B', 'C'>>>,
+        addition.Commutativity<Add<'B', 'C'>, _0>,
+      ],
+      Add<Add<_0, 'B'>, 'C'>
+    >,
+    Add<_0, Add<'B', 'C'>>
+  >>,
+]
-- 
cgit v1.3.1