almost done

2 files changed, 35 insertions, 0 deletions

diff --git a/examples/one_simplex.makkai b/examples/one_simplex.makkai
new file mode 100644
index 0000000..590cf04
--- /dev/null
+++ b/examples/one_simplex.makkai
@@ -0,0 +1,31 @@
+let signature Graph = theory {
+    Vertex :: Set,
+    Edge :: (s : set-of(Vertex)) (t : set-of(Vertex)) -> Set
+}
+
+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 = {
+    .Vertex = F3 :: Set,
+    .Edge = for (s : set-of(Vertex)) (t : set-of(Vertex)),
+              case s of [
+                three0. pt => case t of [ three0. pt => Empty :: Set | three1. pt => Unit :: Set | three2. pt => Unit :: Set ]
+                | three1. pt => case t of [ three0. pt => Empty :: Set | three1. pt => Empty :: Set | three2. pt => Unit :: Set ]
+                | three2. pt => case t of [ three0. pt => Empty :: Set | three1. pt => Empty :: Set | three2. pt => Empty :: Set ]
+              ]
+}
+
+let set OneSimplexEdges = record {
+  source: set-of(oneSimplex .Vertex),
+  target: set-of(oneSimplex .Vertex),
+  connected: set-of(oneSimplex .Edge source target)
+}
+
+let element vertex0 : F3 = three0. {}
+let element vertex1 : F3 = three1. {}
+let element edge01 : set-of(oneSimplex .Edge vertex0 vertex1) = pt
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
+}