1
1
mirror of https://github.com/idris-lang/Idris2.git synced 2024-12-19 17:21:59 +03:00
Idris2/tests/idris2/total008/partial.idr
Edwin Brady 2223d50c3a Skip totality check on case blocks and MNs
These are checked as part of checking the top level names
2020-05-28 15:32:46 +01:00

13 lines
174 B
Idris

import Data.List
interface Foo a where
covering
foo : a -> ()
Foo (Maybe String) where
foo Nothing = ()
foo (Just x) = ()
Foo (Maybe Int) where
foo Nothing = ()