From 89304b27ea81270684810c18d3315c9d399beaf9 Mon Sep 17 00:00:00 2001 From: tslil Date: Tue, 5 May 2026 11:15:07 +0100 Subject: address remaining TODO, fix issues with left-nesting for for and ext, add motivation blurb to the readme --- examples/equality.makkai | 19 +++++++++++++++++++ 1 file changed, 19 insertions(+) create mode 100644 examples/equality.makkai (limited to 'examples/equality.makkai') 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 } -- cgit v1.3.1