Idris2/tests/idris2/linear017/As.idr
Justus Matthiesen 00af44c708
Ignore UseSide annotation in non-linear as-patterns (#2984)
Co-authored-by: Aleksei Volkov <volkov.aa@phystech.edu>
2023-06-01 14:34:57 +01:00

14 lines
382 B
Idris

-- Reduction of https://gist.github.com/AlgebraicWolf/0d921915d7aca032e35831c73c8d04f4
-- See Discord discussion for further context:
-- https://discord.com/channels/827106007712661524/954409815088721920/1108129142756606102
data X : Nat -> Type where
IZ : X Z
IS : (0 n : _) -> X n -> X (S n)
g : (m : Nat) -> X m -> Nat
g (S m@(S m')) (IS .(S m') k) = g (S m') k
g _ _ = 0