Idris2/tests/idris2/coverage004/Cover.idr

%default partial

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
All functions now need to be covering by default This has caught a couple of things in the Idris 2 code base itself. Some tests needed partial annotations too. 2020-05-24 21:58:20 +03:00			`%default partial`

Add test script They don't all pass yet, for minor reasons. Coming shortly... Unfortunately the startup overhead for chez is really noticeable here! 2020-05-19 20:25:18 +03:00			`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`