diff options
| author | Akshay Nair <phenax5@gmail.com> | 2023-12-12 23:44:14 +0530 |
|---|---|---|
| committer | Akshay Nair <phenax5@gmail.com> | 2023-12-12 23:50:38 +0530 |
| commit | 3d49bb583227b7669b638c4bb3e9853feae07ae2 (patch) | |
| tree | e62c83fc83dd18374f3f981c44d0cbef9f4f510e /src/tests.ts | |
| parent | a393765df40744aae68dab943e25bad8175bd5c0 (diff) | |
| download | ts-theorem-provinator-3d49bb583227b7669b638c4bb3e9853feae07ae2.tar.gz ts-theorem-provinator-3d49bb583227b7669b638c4bb3e9853feae07ae2.zip | |
refactor: refactorification
Diffstat (limited to '')
| -rw-r--r-- | src/tests.ts | 28 |
1 files changed, 14 insertions, 14 deletions
diff --git a/src/tests.ts b/src/tests.ts index 04a009a..7f331a6 100644 --- a/src/tests.ts +++ b/src/tests.ts @@ -1,48 +1,48 @@ import { addition, multiplication } from './index'; -import { Add, Multiply, Succ } from './nat'; -import { ApplyRewrite, ChainRewrites, Flip, Eq, VerifyEquation, Equation, assert, Evaluate } from './util'; +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.Commutativity<_0, 'B'>, addition.Identity<'B'>, ], - Add<Add<'0', 'B'>, 'C'> + Add<Add<_0, 'B'>, 'C'> >, Add<'B', 'C'> >>, assert<Eq< ChainRewrites< [ - addition.Commutativity<'0', 'B'>, + addition.Commutativity<_0, 'B'>, addition.Identity<'B'>, - Flip<addition.Identity<Add<'B', 'C'>>>, - addition.Commutativity<Add<'B', 'C'>, '0'>, + Sym<addition.Identity<Add<'B', 'C'>>>, + addition.Commutativity<Add<'B', 'C'>, _0>, ], - Add<Add<'0', 'B'>, 'C'> + Add<Add<_0, 'B'>, 'C'> >, - Add<'0', Add<'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'>>, + 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'>>>, + ApplyRewrite<Add<Add<'A', 'B'>, _0>, addition.Identity<Add<'A', 'B'>>>, Add<'A', 'B'> >>, assert<Eq< - ApplyRewrite<Add<'A', 'B'>, Flip<addition.Identity<Add<'A', 'B'>>>>, - Add<Add<'A', 'B'>, '0'> + 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'>>, + ApplyRewrite<Add<'A', Add<'B', Add<'C', _0>>>, addition.Identity<'C'>>, Add<'A', Add<'B', 'C'>> >>, ] |