Limitation: the type class constraint must be under a scoped implicit
(this is purely for parsing reasons, although I also can't immediately
think of a reason you'd want this except under an implicit...)
Proof state now contains the term in focus, its environment, and a path
through the complete term to reach that sub-term. As a result, large
proof terms are now checked more quickly
Cleaned up a couple of other things on the way...
Now uses the elaborator to generate any necessary extra bindings, using
the same machinery as pattern match elaboration. The end result is that
you no longer need 'using' in a lot of cases (it is still useful if you
want to give explicit types, of course). e.g. this now works as it
stands:
data Elem : a -> Vect n a -> Type where
Here : Elem x (x :: xs)
There : Elem x xs -> Elem x (y :: xs)
isElem : DecEq a => (x : a) -> (xs : _) -> Maybe (Elem x xs)
This should also reduce the number of weird "no such variable" errors
signfificantly. In particular, it fixes#1354
