aboutsummaryrefslogtreecommitdiff
path: root/src/tests/nat.spec.ts
diff options
context:
space:
mode:
authorAkshay Nair <phenax5@gmail.com>2023-12-15 22:36:03 +0530
committerAkshay Nair <phenax5@gmail.com>2023-12-15 22:36:03 +0530
commitefc0358c1e2b52308d3df68aa713cef5dc6e6bfe (patch)
tree40bac1f220895180c1cb99f044ac56eb4ed1ccbb /src/tests/nat.spec.ts
parent3d91b8c0fe73d24e3bcf13e7d7e8079f58975500 (diff)
downloadts-theorem-provinator-efc0358c1e2b52308d3df68aa713cef5dc6e6bfe.tar.gz
ts-theorem-provinator-efc0358c1e2b52308d3df68aa713cef5dc6e6bfe.zip
refactor: moves stuff around
Diffstat (limited to '')
-rw-r--r--src/tests/nat.spec.ts (renamed from src/tests.ts)31
1 files changed, 3 insertions, 28 deletions
diff --git a/src/tests.ts b/src/tests/nat.spec.ts
index 7f331a6..acade6f 100644
--- a/src/tests.ts
+++ b/src/tests/nat.spec.ts
@@ -1,31 +1,6 @@
-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'>>
- >>,
-]
+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 = [