diff --git a/tests/Main.idr b/tests/Main.idr index 809d1f8..4ac0000 100644 --- a/tests/Main.idr +++ b/tests/Main.idr @@ -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", diff --git a/tests/idris2/basic040/Default.idr b/tests/idris2/basic040/Default.idr new file mode 100644 index 0000000..ea7147d --- /dev/null +++ b/tests/idris2/basic040/Default.idr @@ -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)] diff --git a/tests/idris2/basic040/expected b/tests/idris2/basic040/expected new file mode 100644 index 0000000..ca9dd27 --- /dev/null +++ b/tests/idris2/basic040/expected @@ -0,0 +1,2 @@ +1/1: Building Default (Default.idr) +Default> Bye for now! diff --git a/tests/idris2/basic040/run b/tests/idris2/basic040/run new file mode 100755 index 0000000..ba04968 --- /dev/null +++ b/tests/idris2/basic040/run @@ -0,0 +1,3 @@ +echo ":q" | $1 --no-banner Default.idr + +rm -rf build