This makes the elaborator for quasiquotes somewhat more strict, which
prevents unknown names from sneaking in to quasiquotes as well as
causing it to fail if not enough information is provided to solve implicits.
Need to treat appeals to tactics as independent calls to the elaborator,
with known current scope, so don't add implicits until just before
invoking the tactic, and add a final unify/match step to collect any
missing implicits.
This fixes an issue where generated S patterns would sometimes not be
parenthesized, leading to invalid patterns being generated. This
occurred even in tutorial code, like Parity.
This patch does two things:
1. It adds support for a new prover command, :search, with the same
syntax and semantics as the REPL command
2. It makes :search work properly with IDESlave, enabling type search
from the Emacs prover as well as enabling length-limits in the IRC bot
again.
This sort of thing now works:
test : Nat -> Nat
test n = let foo = n
S k = plus foo foo
in k
The bindings must be aligned, and the keyword 'in' (indented however you
like within the 'test' block) terminates the list.
Pattern match alternatives are also supported, for quickly catching
failures:
test2 : Nat -> Nat
test2 n = let foo = n
S k = plus foo foo
| Z => 42
in k
Fixes#1362
Fixes#1367
I'm not yet convinced there isn't still potentially a similar problem
under other forms of ProjCase, but since these only arise in unusual
circumstances at the moment there isn't a problem *yet*!
Check whether any errors introduced by a match are unrecoverable, rather
than merely checking if any more errors are introduced. Otherwise, in
some circumstances (where other problems are resolved by the match) we
might get a type class resolved where it shouldn't be, leading to
mysterious errors later.
Fixes#1365
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