diff options
| author | Akshay Nair <phenax5@gmail.com> | 2023-12-15 22:36:03 +0530 |
|---|---|---|
| committer | Akshay Nair <phenax5@gmail.com> | 2023-12-15 22:36:03 +0530 |
| commit | efc0358c1e2b52308d3df68aa713cef5dc6e6bfe (patch) | |
| tree | 40bac1f220895180c1cb99f044ac56eb4ed1ccbb /src/tests.ts | |
| parent | 3d91b8c0fe73d24e3bcf13e7d7e8079f58975500 (diff) | |
| download | ts-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 = [ |
