Adding missing test files

This commit is contained in:
Edwin Brady 2019-07-09 09:21:57 +02:00
parent 8a1a4ad56d
commit 2487c30232
8 changed files with 58 additions and 0 deletions

View File

@ -0,0 +1,15 @@
foo : (Nat, Nat) -> Nat
foo (Z, Z) = Z
bar : {a : _} -> a -> Nat
bar Z = Z
bar (S _) = S Z
cty : (a : Type) -> a -> Nat
cty Nat Z = Z
cty Nat (S _) = S Z
cty _ x = S (S Z)
badBar : a -> Nat
badBar Z = Z
badBar (S _) = S Z

View File

@ -0,0 +1,11 @@
1/1: Building Cover (Cover.idr)
Cover.idr:14:1--14:8:While processing left hand side of Main.badBar at Cover.idr:14:1--15:1:
Can't match on Z as it has a polymorphic type
Welcome to Idris 2 version 0.0. Enjoy yourself!
Main> Main.foo:
foo (Z, S _)
foo (S _, _)
Main> Main.bar:
bar _
Main> Main.cty: All cases covered
Main> Bye for now!

View File

@ -0,0 +1,4 @@
:missing foo
:missing bar
:missing cty
:q

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

@ -0,0 +1,3 @@
$1 Cover.idr < input
rm -rf build

View File

@ -0,0 +1,12 @@
data Foo : Type -> Type where
IsNat : Foo Nat
IsBool : Foo Bool
okay : a -> Foo a -> Bool
okay Z IsNat = False
okay True IsBool = True
bad : a -> Foo a -> Bool
bad Z IsNat = False
bad True IsBool = True
bad (Just 0) _ = False

View File

@ -0,0 +1,8 @@
1/1: Building Cover (Cover.idr)
Cover.idr:12:1--12:5:While processing left hand side of Main.bad at Cover.idr:12:1--13:1:
Can't match on Just (fromInteger 0) as it has a polymorphic type
Welcome to Idris 2 version 0.0. Enjoy yourself!
Main> Main.okay:
okay (S _) IsNat
okay False IsBool
Main> Bye for now!

View File

@ -0,0 +1,2 @@
:missing okay
:q

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

@ -0,0 +1,3 @@
$1 Cover.idr < input
rm -rf build