diff options
Diffstat (limited to 'examples')
| -rw-r--r-- | examples/alpha_equiv.makkai | 4 | ||||
| -rw-r--r-- | examples/equality.makkai | 19 | ||||
| -rw-r--r-- | examples/ext_codomain.makkai | 5 | ||||
| -rw-r--r-- | examples/inline_nested.makkai | 9 | ||||
| -rw-r--r-- | examples/nested_for.makkai | 3 |
5 files changed, 40 insertions, 0 deletions
diff --git a/examples/alpha_equiv.makkai b/examples/alpha_equiv.makkai new file mode 100644 index 0000000..2ae067a --- /dev/null +++ b/examples/alpha_equiv.makkai @@ -0,0 +1,4 @@ +let signature S = (n : Nat) -> Set +let signature T = (m : Nat) -> Set +let instance i :: S = for (x : Nat), (Nat :: Set) +let instance j :: T = i 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 } diff --git a/examples/ext_codomain.makkai b/examples/ext_codomain.makkai new file mode 100644 index 0000000..da0ddae --- /dev/null +++ b/examples/ext_codomain.makkai @@ -0,0 +1,5 @@ +let signature S = (x : Nat) -> theory { G :: Set } + +let instance s :: S = for (x : Nat), { .G = (Nat :: Set) } + +let set NatAgain = set-of((s 42) .G) diff --git a/examples/inline_nested.makkai b/examples/inline_nested.makkai new file mode 100644 index 0000000..e891349 --- /dev/null +++ b/examples/inline_nested.makkai @@ -0,0 +1,9 @@ +let signature Outer = theory { + Inner :: theory { F :: Set } +} + +let instance my_outer :: Outer = { + .Inner = { .F = (Nat :: Set) } +} + +let set MyF = set-of(my_outer .Inner .F) diff --git a/examples/nested_for.makkai b/examples/nested_for.makkai new file mode 100644 index 0000000..b3618cc --- /dev/null +++ b/examples/nested_for.makkai @@ -0,0 +1,3 @@ +let signature F = (n : Nat) -> (m : Nat) -> Set +let instance f :: F = for (n : Nat), for (m : Nat), (Nat :: Set) +let set Result = set-of(f 1 2) |