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.ts | 85 ------------------------------------------------------------
 1 file changed, 85 deletions(-)
 delete mode 100644 src/tests.ts

(limited to 'src/tests.ts')

diff --git a/src/tests.ts b/src/tests.ts
deleted file mode 100644
index 7f331a6..0000000
--- a/src/tests.ts
+++ /dev/null
@@ -1,85 +0,0 @@
-import { addition, multiplication } from './index';
-import { Add, Multiply, Succ, _0 } from './nat';
-import { ApplyRewrite, ChainRewrites, Sym, Eq, VerifyEquation, Equation, assert, Evaluate } from './util';
-
-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'>>
-  >>,
-]
-
-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