[ test ] for the perf regression

idris-lang · Jul 26, 2024 · c25ed95 · c25ed95
1 parent 2667723
commit c25ed95
Show file tree

Hide file tree

Showing 3 changed files with 15 additions and 0 deletions.
diff --git a/tests/idris2/reg/reg054/Issue3354.idr b/tests/idris2/reg/reg054/Issue3354.idr
@@ -0,0 +1,12 @@
+import Data.Fin
+
+covering
+g : Fin 64 -> Unit
+g FZ      = ()
+g (FS i') = g $ weaken i'
+
+
+total
+g' : Fin 64 -> Unit
+g' FZ        = ()
+g' i@(FS i') = g' $ assert_smaller i $ weaken i'
diff --git a/tests/idris2/reg/reg054/expected b/tests/idris2/reg/reg054/expected
@@ -0,0 +1 @@
+1/1: Building Issue3354 (Issue3354.idr)
diff --git a/tests/idris2/reg/reg054/run b/tests/idris2/reg/reg054/run
@@ -0,0 +1,2 @@
+. ../../../testutils.sh
+check Issue3354.idr