tests: add fixtures

aya-prover · Jan 6, 2023 · ef94733 · ef94733
1 parent 92be278
commit ef94733
Show file tree

Hide file tree

Showing 2 changed files with 9 additions and 1 deletion.
diff --git a/base/src/test/resources/failure/holes/issue747.aya.txt b/base/src/test/resources/failure/holes/issue747.aya.txt
@@ -11,7 +11,7 @@ Goal: Goal of type
       Context:
         {a : Nat}
       To ensure confluence:
-        Given (i ⇒ _), we should have: 0
+        Given (_ ⇒ 0, i ⇒ _), we should have: 0
 
 In file $FILE:11:13 ->
 

diff --git a/base/src/test/resources/success/src/Prop.aya b/base/src/test/resources/success/src/Prop.aya
@@ -1,3 +1,5 @@
+open import Paths
+
 open struct Squash (A: Type): Prop
   | value: A
 
@@ -9,3 +11,9 @@ def squashElim {A: Type} {P: Prop} (f: A -> P) (squash: Squash A): P => f squash
 def squash2Elim {A: Type} {P: Prop} (f: A -> P) (squash: Squash2 A): P
   | f, (squash a) => f a
 
+open data Carry (A : Prop) : Type
+| carry A
+
+open data Bool : Prop | true | false
+
+def check : carry true = carry false => idp