mirror of
https://github.com/edwinb/Idris2-boot.git
synced 2024-08-17 03:40:33 +03:00
[ test ] add test for defaulting peculiarity (#376)
This commit is contained in:
parent
6f4a36e84b
commit
306aea32b8
@ -34,7 +34,7 @@ idrisTests
|
||||
"basic021", "basic022", "basic023", "basic024", "basic025",
|
||||
"basic026", "basic027", "basic028", "basic029", "basic030",
|
||||
"basic031", "basic032", "basic033", "basic034", "basic035",
|
||||
"basic036", "basic037", "basic038", "basic039",
|
||||
"basic036", "basic037", "basic038", "basic039", "basic040",
|
||||
-- Coverage checking
|
||||
"coverage001", "coverage002", "coverage003", "coverage004",
|
||||
"coverage005", "coverage006",
|
||||
|
21
tests/idris2/basic040/Default.idr
Normal file
21
tests/idris2/basic040/Default.idr
Normal file
@ -0,0 +1,21 @@
|
||||
module Default
|
||||
|
||||
happyPairs : List (Nat, Char)
|
||||
happyPairs = map (uncurry $ \ c, n => (n, c)) [('a', 1)]
|
||||
|
||||
-- In Idris1 `sadPairs` is rejected with the following error:
|
||||
-- |
|
||||
-- 10 | sadPairs = map (\ (c, n) => (n, c)) [('a', 1)]
|
||||
-- | ~~
|
||||
-- When checking right hand side of Default.case block in sadPairs at Default.idr:10:19-24 with expected type
|
||||
-- (Nat, Char)
|
||||
|
||||
-- When checking argument a to constructor Builtins.MkPair:
|
||||
-- Type mismatch between
|
||||
-- Integer (Type of n)
|
||||
-- and
|
||||
-- Nat (Expected type)
|
||||
|
||||
|
||||
sadPairs : List (Nat, Char)
|
||||
sadPairs = map (\ (c, n) => (n, c)) [('a', 1)]
|
2
tests/idris2/basic040/expected
Normal file
2
tests/idris2/basic040/expected
Normal file
@ -0,0 +1,2 @@
|
||||
1/1: Building Default (Default.idr)
|
||||
Default> Bye for now!
|
3
tests/idris2/basic040/run
Executable file
3
tests/idris2/basic040/run
Executable file
@ -0,0 +1,3 @@
|
||||
echo ":q" | $1 --no-banner Default.idr
|
||||
|
||||
rm -rf build
|
Loading…
Reference in New Issue
Block a user