aboutsummaryrefslogtreecommitdiff
path: root/src/tests.ts
diff options
context:
space:
mode:
Diffstat (limited to 'src/tests.ts')
-rw-r--r--src/tests.ts14
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'>>
+ >>,
+ ]
}