mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-26 13:11:30 +03:00
9 lines
311 B
Plaintext
9 lines
311 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
|