mirror of
https://github.com/ilyakooo0/Idris-dev.git
synced 2024-09-17 11:47:20 +03:00
da914af83e
We've always said that the rules for binding names in patterns are the same as the rules for binding names in implicits, i.e. a name beginning with a lower case letter, not applied to anything, will be bound implicitly, or treated as a pattern variable. This hasn't actually always been quite true, even though it was supposed to be... Correspondingly, added a warning for constructor names which may be unexpectedly bound implicitly. This patch changes the pattern binding rules so that it is the case. Fixes #2653
13 lines
303 B
Idris
13 lines
303 B
Idris
|
|
data Parity : Nat -> Type where
|
|
Even : Parity (n + n)
|
|
Odd : Parity (S (n + n))
|
|
|
|
parity : (n:Nat) -> Parity n
|
|
parity Z = Even {n=Z}
|
|
parity (S Z) = Odd {n=Z}
|
|
parity (S (S k)) with (parity k)
|
|
parity (S (S (j + j))) | Even = Even {n=S j}
|
|
parity (S (S (S (j + j)))) | Odd = Odd {n=S j}
|
|
|