add test file

idris-lang · Oct 2, 2024 · ea9433a · ea9433a
1 parent bc21157
commit ea9433a
Show file tree

Hide file tree

Showing 3 changed files with 13 additions and 0 deletions.
diff --git a/tests/idris2/operators/operators004/Test.idr b/tests/idris2/operators/operators004/Test.idr
@@ -0,0 +1,9 @@
+import Data.Vect
+
+typebind
+Exists : (t : Type) -> (t -> Type) -> Type
+Exists = DPair
+
+val : Exists (n : Nat) | Vect n Nat
+val = (4 ** [0,1,2,3])
+
diff --git a/tests/idris2/operators/operators004/expected b/tests/idris2/operators/operators004/expected
@@ -0,0 +1 @@
+1/1: Building Test (Test.idr)
diff --git a/tests/idris2/operators/operators004/run b/tests/idris2/operators/operators004/run
@@ -0,0 +1,3 @@
+. ../../../testutils.sh
+
+check Test.idr