idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-11-28 02:23:44 +03:00
Code Issues Projects Releases Wiki Activity

[ test ] non-terminating function from issue #2448

Browse Source
This commit is contained in:
Justus Matthiesen 2023-02-07 16:52:07 +00:00 committed by G. Allais
parent 7eed472ac5
commit 6edbfc59a5
4 changed files with 22 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
tests/Main.idr
View File

@ -226,7 +226,7 @@ idrisTestsTotality = MkTestPool "Totality checking" [] Nothing
"total001", "total002", "total003", "total004", "total005",
"total006", "total007", "total008", "total009", "total010",
"total011", "total012", "total013", "total014", "total015",
"total016", "total017"
"total016", "total017", "total018"
]
-- This will only work with an Idris compiled via Chez or Racket, but at

7
tests/idris2/total018/Issue2448.idr Normal file
View File

@ -0,0 +1,7 @@
-- https://github.com/idris-lang/Idris2/issues/2448#issuecomment-1117103496
%default total
boom : Nat -> Void
boom (S x) = boom x
boom x = boom x

11
tests/idris2/total018/expected Normal file
View File

@ -0,0 +1,11 @@
1/1: Building Issue2448 (Issue2448.idr)
Error: boom is not total, possibly not terminating due to recursive path Main.boom
Issue2448:5:1--5:19
1 | -- https://github.com/idris-lang/Idris2/issues/2448#issuecomment-1117103496
2 |
3 | %default total
4 |
5 | boom : Nat -> Void
^^^^^^^^^^^^^^^^^^

3
tests/idris2/total018/run Executable file
View File

@ -0,0 +1,3 @@
rm -rf build
$1 --no-color --console-width 0 --no-banner --check Issue2448.idr