diff options
Diffstat (limited to 'src/tests.ts')
| -rw-r--r-- | src/tests.ts | 14 |
1 files changed, 13 insertions, 1 deletions
diff --git a/src/tests.ts b/src/tests.ts index 5c066dc..04a009a 100644 --- a/src/tests.ts +++ b/src/tests.ts @@ -1,6 +1,6 @@ import { addition, multiplication } from './index'; import { Add, Multiply, Succ } from './nat'; -import { ApplyRewrite, ChainRewrites, Flip, Eq, VerifyEquation, Equation, assert } from './util'; +import { ApplyRewrite, ChainRewrites, Flip, Eq, VerifyEquation, Equation, assert, Evaluate } from './util'; export type specChainRewrites = [ assert<Eq< @@ -70,4 +70,16 @@ export namespace multiplication_spec { Multiply<Multiply<'B', 'A'>, 'C'> >>, ] + export type specDistributivity = [ + assert<Eq< + Evaluate<multiplication.Distributivity<'A', 'B', 'C'>>, + Add<Multiply<'A', 'C'>, Multiply<'B', 'C'>> + >>, + ] + export type specAssociativity = [ + assert<Eq< + Evaluate<multiplication.Associativity<'A', 'B', 'C'>>, + Multiply<'A', Multiply<'B', 'C'>> + >>, + ] } |
