TEST: add @refparo test, fix #2

aya-prover · Aug 25, 2021 · e4948a9 · e4948a9
1 parent a7cf6f5
commit e4948a9
Showing 1 changed file with 15 additions and 0 deletions.
diff --git a/base/src/test/resources/success/refparo1.aya b/base/src/test/resources/success/refparo1.aya
@@ -0,0 +1,15 @@
+-- #2 in public repo
+data Entity : Set
+  | john
+
+struct EventT : Set
+  | agentT : Set
+
+struct Event (t : EventT) : Set
+  | agent : t.agentT
+
+data Run (e : Event (new EventT { | agentT => Entity })) : Set
+  | (john) => run1
+
+def mkVerb {t : EventT} (p : Event t -> Set) : (Event t -> Set) -> Set
+  => \f => Sig (e : Event t) ** (Sig (p e) ** (f e))