From c25ed953a5da4675956735ff3b25386ec5485815 Mon Sep 17 00:00:00 2001 From: Guillaume Allais Date: Fri, 26 Jul 2024 13:58:24 +0100 Subject: [PATCH] [ test ] for the perf regression --- tests/idris2/reg/reg054/Issue3354.idr | 12 ++++++++++++ tests/idris2/reg/reg054/expected | 1 + tests/idris2/reg/reg054/run | 2 ++ 3 files changed, 15 insertions(+) create mode 100644 tests/idris2/reg/reg054/Issue3354.idr create mode 100644 tests/idris2/reg/reg054/expected create mode 100644 tests/idris2/reg/reg054/run diff --git a/tests/idris2/reg/reg054/Issue3354.idr b/tests/idris2/reg/reg054/Issue3354.idr new file mode 100644 index 0000000000..5dfb4eb947 --- /dev/null +++ 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 new file mode 100644 index 0000000000..72b6431c2c --- /dev/null +++ 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 new file mode 100644 index 0000000000..9e5036f0ee --- /dev/null +++ b/tests/idris2/reg/reg054/run @@ -0,0 +1,2 @@ +. ../../../testutils.sh +check Issue3354.idr