diff options
Diffstat (limited to '')
| -rw-r--r-- | src/tests/nat.spec.ts (renamed from src/tests.ts) | 31 | ||||
| -rw-r--r-- | src/tests/theorem.spec.ts | 28 |
2 files changed, 31 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 = [ 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'>> + >>, +] |