From 1b4abb8fdd81f6de2166ef3f064a77fd5622fe83 Mon Sep 17 00:00:00 2001 From: tslil Date: Wed, 6 May 2026 11:21:22 +0100 Subject: clean up examples vs tests --- examples/equality.makkai | 21 ++++++++++++--------- 1 file changed, 12 insertions(+), 9 deletions(-) (limited to 'examples/equality.makkai') diff --git a/examples/equality.makkai b/examples/equality.makkai index a9b3368..ede2a54 100644 --- a/examples/equality.makkai +++ b/examples/equality.makkai @@ -4,16 +4,19 @@ 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 signature SetWitRelation = theory { + Carrier :: Set, + Relation :: (x : set-of(Carrier)) (y: set-of(Carrier)) -> Set + +} +let instance eqThree :: SetWitRelation = { + .Carrier = Three :: Set, + .Relation = for (x: Three) (y: Three), + 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 set Diagonal = record { x : set-of(eqThree .Carrier), y : set-of(eqThree .Carrier), equal : set-of((eqThree .Relation) x y) } 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