From a52308d77d507490ea3599cf724d1a66cb48704b Mon Sep 17 00:00:00 2001
From: Edwin Brady <ecb10@st-andrews.ac.uk>
Date: Mon, 29 Jun 2020 15:13:42 +0100
Subject: [PATCH] Add test files

---
 tests/idris2/reg028/Test.idr | 16 ++++++++++++++++
 tests/idris2/reg028/expected |  1 +
 tests/idris2/reg028/run      |  3 +++
 3 files changed, 20 insertions(+)
 create mode 100644 tests/idris2/reg028/Test.idr
 create mode 100644 tests/idris2/reg028/expected
 create mode 100755 tests/idris2/reg028/run

diff --git a/tests/idris2/reg028/Test.idr b/tests/idris2/reg028/Test.idr
new file mode 100644
index 000000000..6ea3b1535
--- /dev/null
+++ b/tests/idris2/reg028/Test.idr
@@ -0,0 +1,16 @@
+module Test
+
+data Dummy : (lbl : Type) -> (st : List lbl) -> Type -> Type where
+  MkDummy : a -> Dummy b st a
+
+
+public export
+interface IxPure (f : (lbl : Type) -> (st : List lbl) -> Type -> Type)
+          where
+  ixPure : a -> f lbl st a
+
+IxPure Dummy where
+  ixPure = MkDummy
+
+pure12 : Dummy String xs Nat
+pure12 = ixPure Z
diff --git a/tests/idris2/reg028/expected b/tests/idris2/reg028/expected
new file mode 100644
index 000000000..31e5db7f3
--- /dev/null
+++ b/tests/idris2/reg028/expected
@@ -0,0 +1 @@
+1/1: Building Test (Test.idr)
diff --git a/tests/idris2/reg028/run b/tests/idris2/reg028/run
new file mode 100755
index 000000000..ad0ea8fa4
--- /dev/null
+++ b/tests/idris2/reg028/run
@@ -0,0 +1,3 @@
+$1 --check Test.idr
+
+rm -rf build