@kha We have a few parsers that invoke `tokenFn`, and return error
depending of what is on the top of the stack (e.g., `ident`).
These parsers were not restoring the stack size when reporting errord,
and messing up the error recovery. We never notice the problem because
operators such as <|> restore the stack size, and we were not trying
to elaborate syntacticly incorrect terms.
@Kha after I enabled elaboration on syntactically incorrect terms, the
fallback is activated more often, and the raw term seems to have
little value for most users, and it is just scary.
Not sure whether the flag is a good idea, but it produces are more
user friendly output.
change the generated to code recursively call the fields of recursive
and mutually recursive types. Currently, this can emit `partial`
functions due to lacking structural recursion. The code is prepared,
however, for the full implementation and can be trivially turned into
code generating non-`partial` functions
@Kha This commit addresses an issue reported by Kevin. Holes and tactic
blocks represent a discontinuity in the elaboration process.
By introducing inaccessible variables (or "things" as Kevin calls
them), we create error message that are harder to understand (see
affected test), and goals where we didn't allow the user to select the
variable name and/or eagerly unfolded a definition.
BTW, I first considered using "reducible" setting when deciding
whether to insert implicit lambdas or not. This is a bad idea.
See `monotone.lean` test. The decision should not depend on
reducibility status, but whether there is "discontinuity" on the
elaboration process or not. As Kevin pointed out,
"introducing implicits work great if you finish the job".
If generated type is not correct, we should abort "discriminant
refinement", and use the original error message because users may
be confused by a type error on something they did not write.
