diff options
Diffstat (limited to 'examples/equality.makkai')
| -rw-r--r-- | examples/equality.makkai | 19 |
1 files changed, 19 insertions, 0 deletions
diff --git a/examples/equality.makkai b/examples/equality.makkai new file mode 100644 index 0000000..a9b3368 --- /dev/null +++ b/examples/equality.makkai @@ -0,0 +1,19 @@ +let set Empty = variant[] +let set Unit = record {} +let element pt : Unit = {} + +let set Three = variant [ zero : Unit | one : Unit | two : Unit ] + +let signature EqS = (x : Three) (y: Three) -> theory { E :: Set } +let instance eqThree :: EqS = for (x: Three) (y: Three), { + .E = case x of [ zero. z => case y of [ zero. w => Unit :: Set | one. w => Empty :: Set | two. w => Empty :: Set ] + | one. z => case y of [ zero. w => Empty :: Set | one. w => Unit :: Set | two. w => Empty :: Set ] + | two. z => case y of [ zero. w => Empty :: Set | one. w => Empty :: Set | two. w => Unit :: Set ] + ] +} + +let set Diagonal = record { x : Three, y : Three, equal : set-of((eqThree x y) .E) } + +let element oneEqualsOne : Diagonal = { .x = one. pt, .y = one. pt, .equal = pt } + +let element oopsOneEqualsTwo : Diagonal = { .x = one. pt, .y = two. pt, .equal = pt } |