From ea9433a506cc9a9cfa3d259d5881ddc58a165589 Mon Sep 17 00:00:00 2001 From: Andre Videla Date: Wed, 2 Oct 2024 22:55:39 +0100 Subject: [PATCH] add test file --- tests/idris2/operators/operators004/Test.idr | 9 +++++++++ tests/idris2/operators/operators004/expected | 1 + tests/idris2/operators/operators004/run | 3 +++ 3 files changed, 13 insertions(+) create mode 100644 tests/idris2/operators/operators004/Test.idr create mode 100644 tests/idris2/operators/operators004/expected create mode 100755 tests/idris2/operators/operators004/run diff --git a/tests/idris2/operators/operators004/Test.idr b/tests/idris2/operators/operators004/Test.idr new file mode 100644 index 0000000000..b9ac279e8a --- /dev/null +++ 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 new file mode 100644 index 0000000000..31e5db7f32 --- /dev/null +++ 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 new file mode 100755 index 0000000000..d35387bb39 --- /dev/null +++ b/tests/idris2/operators/operators004/run @@ -0,0 +1,3 @@ +. ../../../testutils.sh + +check Test.idr