Idris2/tests/idris2/reg022/case.idr

mirror of https://github.com/idris-lang/Idris2.git synced 2024-12-25 04:33:45 +03:00
-- Previously this gave an 'unreachable case warning' and evaluated
-- to the first case! Should give foo : Nat -> Nat
foo : (x : Nat) -> case S x of
                        Z => Nat -> Nat
                        (S k) => Nat
Fix case trees at multiplicity zero Can't ignore a constructor a multiplicity zero if the whole function is multiplicity zero 2020-06-06 22:40:10 +03:00			`-- Previously this gave an 'unreachable case warning' and evaluated`
			`-- to the first case! Should give foo : Nat -> Nat`
			`foo : (x : Nat) -> case S x of`
			`Z => Nat -> Nat`
			`(S k) => Nat`