Idris2-boot/tests/ttimp/qtt003/QTTEq.yaff

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
Add a test for non linear LHS 2019-05-19 22:30:27 +03:00			`data Eq : $a -> $b -> Type where`
			`Refl : Eq $x $x`

Check pattern variables don't unify with things This is bad because it means a pattern variable isn't actually a variable, but rather has a specific value! 2019-05-25 22:18:43 +03:00			`okay : {p : $a -> Type} -> (1 x : $a) -> (1 y : $a) -> (1 prf : Eq x y) ->`
Add a test for non linear LHS 2019-05-19 22:30:27 +03:00			`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.`
Implement dot patterns Like Idris 1, these are implicitly added on encountering a repeated name or a non-constructor application. Unlike Idris 1 (and Blodwen) they are checking by unification rather than matching (which means in particular that function argument names can't be bound in dot patterns) which is slightly less expressive, but better overall because matching is potentially more error prone. 2019-05-25 20:39:21 +03:00			`okay $x $x Refl $q = q`