aboutsummaryrefslogtreecommitdiff
path: root/examples/signature_param.makkai
diff options
context:
space:
mode:
authortslil <tslil@posteo.de>2026-05-04 17:52:04 +0100
committertslil <tslil@posteo.de>2026-05-04 18:26:43 +0100
commit90e451893671ceebaa37fcb634b5d7a3f153ba70 (patch)
treeb7d21bc968fed9141c74b6cb00ec3a3ae1e577ed /examples/signature_param.makkai
parent3ce914fdc62923c92812037297aee64747a9867e (diff)
almost done
Diffstat (limited to 'examples/signature_param.makkai')
-rw-r--r--examples/signature_param.makkai4
1 files changed, 4 insertions, 0 deletions
diff --git a/examples/signature_param.makkai b/examples/signature_param.makkai
new file mode 100644
index 0000000..9dae31b
--- /dev/null
+++ b/examples/signature_param.makkai
@@ -0,0 +1,4 @@
+let signature S = theory {
+ F :: (x : Nat) (y : Bool) -> Set,
+ G :: (z : set-of(F 3 4)) -> Set // this sould fail
+}