diff options
| author | Akshay Nair <phenax5@gmail.com> | 2023-12-10 17:33:01 +0530 |
|---|---|---|
| committer | Akshay Nair <phenax5@gmail.com> | 2023-12-10 17:33:01 +0530 |
| commit | f724285d1d3cea85128069bcdf04e4c6af9c7a39 (patch) | |
| tree | ee73c1b85a4af63f6e553bbc8c3379d406e8e3ee /src/tests.ts | |
| parent | f6e26212620de411e082cbd52379075ea5a99032 (diff) | |
| download | ts-theorem-provinator-f724285d1d3cea85128069bcdf04e4c6af9c7a39.tar.gz ts-theorem-provinator-f724285d1d3cea85128069bcdf04e4c6af9c7a39.zip | |
adds associativity for a=0
Diffstat (limited to '')
| -rw-r--r-- | src/tests.ts | 42 |
1 files changed, 40 insertions, 2 deletions
diff --git a/src/tests.ts b/src/tests.ts index 8c379e8..b4fc214 100644 --- a/src/tests.ts +++ b/src/tests.ts @@ -1,6 +1,7 @@ -import { Add, ApplyRewrite, Commutativity, Flip, Identity } from './index'; +import { Add, Assoc0, Commutativity, Identity } from './index'; +import { ApplyRewrite, ChainRewrites, Flip } from './util'; -type Eq<a, b> = ([a] extends [b] ? ([b] extends [a] ? true : false) : false) & { a: a; b: b }; +type Eq<a, b> = ([a] extends [b] ? ([b] extends [a] ? true : false & { a: a; b: b }) : false & { a: a; b: b }); type assert<T extends true> = T; export type _testCases = { @@ -22,6 +23,7 @@ export type _testCases = { Add<'A', Add<'B', 'C'>> >>, ], + Commutativity: [ assert<Eq< ApplyRewrite<Add<'A', 'B'>, Commutativity<'A', 'B'>>, @@ -36,4 +38,40 @@ export type _testCases = { Add<'A', Add<'C', 'B'>> >>, ], + + ChainRewrites: [ + assert<Eq< + ChainRewrites< + [ + Commutativity<'0', 'B'>, + Identity<'B'>, + ], + Add<Add<'0', 'B'>, 'C'> + >, + Add<'B', 'C'> + >>, + assert<Eq< + ChainRewrites< + [ + Commutativity<'0', 'B'>, + Identity<'B'>, + Flip<Identity<Add<'B', 'C'>>>, + Commutativity<Add<'B', 'C'>, '0'>, + ], + Add<Add<'0', 'B'>, 'C'> + >, + Add<'0', Add<'B', 'C'>> + >>, + ], + + Assoc0: [ + assert<Eq< + ApplyRewrite<Add<Add<'0', 'B'>, 'C'>, Assoc0<'B', 'C'>>, + Add<'0', Add<'B', 'C'>> + >>, + assert<Eq< + ApplyRewrite<Add<Add<'0', Add<'A', 'B'>>, 'C'>, Assoc0<Add<'A', 'B'>, 'C'>>, + Add<'0', Add<Add<'A', 'B'>, 'C'>> + >>, + ], }; |
