3 Commits

Author	SHA1	Message	Date
Edwin Brady	c65285a1f6	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 20:18:43 +01:00
Edwin Brady	6c7f13d128	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 18:39:21 +01:00
Edwin Brady	d256dbf5ec	Add a test for non linear LHS	2019-05-19 20:30:27 +01:00