From ef947332234082fdfae82c769eab91b17fd57b08 Mon Sep 17 00:00:00 2001
From: ice1000 <ice1000kotlin@foxmail.com>
Date: Fri, 6 Jan 2023 22:54:19 +0000
Subject: [PATCH] tests: add fixtures

---
 base/src/test/resources/failure/holes/issue747.aya.txt | 2 +-
 base/src/test/resources/success/src/Prop.aya           | 8 ++++++++
 2 files changed, 9 insertions(+), 1 deletion(-)

diff --git a/base/src/test/resources/failure/holes/issue747.aya.txt b/base/src/test/resources/failure/holes/issue747.aya.txt
index 1c62c2cba9..c6518135ef 100644
--- 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
index 3e9b66037e..380478f99e 100644
--- 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