idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-10-26 14:09:09 +03:00
Code Issues Projects Releases Wiki Activity

[ test ] for the perf regression

Browse Source
This commit is contained in:
Guillaume Allais 2024-07-26 13:58:24 +01:00 committed by G. Allais
parent adf284260b
commit 3f76bfdd6f
3 changed files with 15 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

12
tests/idris2/reg/reg054/Issue3354.idr Normal file
View File

@ -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'

1
tests/idris2/reg/reg054/expected Normal file
View File

@ -0,0 +1 @@
1/1: Building Issue3354 (Issue3354.idr)

2
tests/idris2/reg/reg054/run Normal file
View File

@ -0,0 +1,2 @@
. ../../../testutils.sh
check Issue3354.idr