diff options
Diffstat (limited to 'examples')
| -rw-r--r-- | examples/equality.makkai | 2 | ||||
| -rw-r--r-- | examples/tests/test_projection.makkai | 10 |
2 files changed, 11 insertions, 1 deletions
diff --git a/examples/equality.makkai b/examples/equality.makkai index 86b81ae..294dafc 100644 --- a/examples/equality.makkai +++ b/examples/equality.makkai @@ -54,7 +54,7 @@ let signature NeqParticular = theory { Neq :: (r: set-of((SE .Relation) (element-of(A)) (element-of(B)))) -> <Empty> } -let instance zeroNeqOne :: NeqParticular = { +let instance zeroNeqOneAgain :: NeqParticular = { .SE = eqTwo, .A = <zero. pt>, .B = <one. pt>, diff --git a/examples/tests/test_projection.makkai b/examples/tests/test_projection.makkai new file mode 100644 index 0000000..2c4ce23 --- /dev/null +++ b/examples/tests/test_projection.makkai @@ -0,0 +1,10 @@ +let signature S = theory { + A :: Set, + Point :: <A>, + B :: (x : set-of(A)) -> Set +} + +let signature T = theory { + SI :: S, + F :: (r: set-of((SI .B) (element-of(SI .Point)))) -> Set +} |