idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-12-25 20:51:43 +03:00
Code Issues Projects Releases Wiki Activity

[ test ] case for #484

Browse Source 
This issue was fixed by #1081
This commit is contained in:
Guillaume ALLAIS 2021-02-22 16:04:04 +00:00
parent 505224e9fc
commit 741960f0d1
3 changed files with 27 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

12
tests/idris2/coverage012/Issue484.idr Normal file
View File

@ -0,0 +1,12 @@
%default covering
data Three = Vrai | Faux | Indef
getType : Three -> Type
getType Vrai = Unit
getType Faux = Unit
getType Indef = Void
swap : (t : Three) -> getType t -> Three
swap Indef _ impossible
swap Vrai () = Faux

14
tests/idris2/coverage012/expected
View File

@ -10,3 +10,17 @@ Issue899.idr:3:1--3:46
Missing cases: Missing cases:
zeroImpossible 0 _ zeroImpossible 0 _
1/1: Building Issue484 (Issue484.idr)
Error: swap is not covering.
Issue484.idr:10:1--10:41
06 | getType Vrai = Unit
07 | getType Faux = Unit
08 | getType Indef = Void
09 |
10 | swap : (t : Three) -> getType t -> Three
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Missing cases:
swap Faux _

1
tests/idris2/coverage012/run
View File

@ -1,3 +1,4 @@
$1 --no-color --console-width 0 --check Issue899.idr $1 --no-color --console-width 0 --check Issue899.idr
$1 --no-color --console-width 0 --check Issue484.idr
rm -rf build rm -rf build