mirror of
https://github.com/edwinb/Idris2-boot.git
synced 2024-09-19 20:07:20 +03:00
c65285a1f6
This is bad because it means a pattern variable isn't actually a variable, but rather has a specific value!
9 lines
312 B
Plaintext
9 lines
312 B
Plaintext
data Eq : $a -> $b -> Type where
|
|
Refl : Eq $x $x
|
|
|
|
okay : {p : $a -> Type} -> (1 x : $a) -> (1 y : $a) -> (1 prf : Eq x y) ->
|
|
p x -> p y
|
|
-- Should fail on the LHS, before even getting to the RHS, because
|
|
-- after elaboration 'x' appears twice even though it is linearly bound.
|
|
okay $x $x Refl $q = q
|