diff options
Diffstat (limited to 'examples')
| -rw-r--r-- | examples/equality.makkai | 21 | ||||
| -rw-r--r-- | examples/one_simplex.makkai | 2 | ||||
| -rw-r--r-- | examples/tests/test_alpha_equiv.makkai (renamed from examples/alpha_equiv.makkai) | 0 | ||||
| -rw-r--r-- | examples/tests/test_ext_codomain.makkai (renamed from examples/ext_codomain.makkai) | 0 | ||||
| -rw-r--r-- | examples/tests/test_inline_nested.makkai (renamed from examples/inline_nested.makkai) | 0 | ||||
| -rw-r--r-- | examples/tests/test_nested_for.makkai (renamed from examples/nested_for.makkai) | 0 | ||||
| -rw-r--r-- | examples/tests/test_signature_merge.makkai (renamed from examples/signature_merge.makkai) | 0 | ||||
| -rw-r--r-- | examples/tests/test_signature_param.makkai (renamed from examples/signature_param.makkai) | 0 |
8 files changed, 12 insertions, 11 deletions
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 } diff --git a/examples/one_simplex.makkai b/examples/one_simplex.makkai index 590cf04..f7e7bff 100644 --- a/examples/one_simplex.makkai +++ b/examples/one_simplex.makkai @@ -6,8 +6,6 @@ let signature Graph = theory { let set Empty = variant[] let set Unit = record{} let element pt : Unit = {} -let set F1 = variant [ one0 : Unit ] -let set F2 = variant [ two0 : Unit | two1 : Unit ] let set F3 = variant [ three0 : Unit | three1 : Unit | three2: Unit ] let instance oneSimplex :: Graph = { diff --git a/examples/alpha_equiv.makkai b/examples/tests/test_alpha_equiv.makkai index 2ae067a..2ae067a 100644 --- a/examples/alpha_equiv.makkai +++ b/examples/tests/test_alpha_equiv.makkai diff --git a/examples/ext_codomain.makkai b/examples/tests/test_ext_codomain.makkai index da0ddae..da0ddae 100644 --- a/examples/ext_codomain.makkai +++ b/examples/tests/test_ext_codomain.makkai diff --git a/examples/inline_nested.makkai b/examples/tests/test_inline_nested.makkai index e891349..e891349 100644 --- a/examples/inline_nested.makkai +++ b/examples/tests/test_inline_nested.makkai diff --git a/examples/nested_for.makkai b/examples/tests/test_nested_for.makkai index b3618cc..b3618cc 100644 --- a/examples/nested_for.makkai +++ b/examples/tests/test_nested_for.makkai diff --git a/examples/signature_merge.makkai b/examples/tests/test_signature_merge.makkai index 5f575d5..5f575d5 100644 --- a/examples/signature_merge.makkai +++ b/examples/tests/test_signature_merge.makkai diff --git a/examples/signature_param.makkai b/examples/tests/test_signature_param.makkai index 9dae31b..9dae31b 100644 --- a/examples/signature_param.makkai +++ b/examples/tests/test_signature_param.makkai |