mirror of
https://github.com/edwinb/Idris2-boot.git
synced 2024-11-23 11:12:33 +03:00
9 lines
309 B
Plaintext
9 lines
309 B
Plaintext
data Eq : $a -> $b -> Type where
|
|
Refl : Eq $x $x
|
|
|
|
okay : {p : $a -> $b} -> (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 Refl $q = q
|