Bad info displayed from Lean

[joneugster]

There are already some issues about this, which should be linked here in future.

Some info displayed by lean is very confusing. Overwrite that behaviour or change it in Lean:

• rw error message
• hover over +
• namespaces in lemma statement
• inaccessible hypotheses in lemma statement

[Trequetrum]

It doesn't feel like a high priority at all, but it would be nice to have a principled way to intercept and change error messages.

While Lean has no recourse to exposing details about it's type theory in the error messages, Lean4Game games/worlds/levels might have extra information about the sorts of errors a user can be expected to encounter that wouldn't make any sense to upstream to Lean itself.

For example, the flavor text in the Intro to Logic Game tends to talk about things being "evidence for" instead of "a proof of" or "A term of type," so an error like:

argument
  s
has type
  S : Prop
but is expected to have type
  P : Prop

introduces the overhead of explaining that this means "the goal is expecting evidence for P, but you've given it evidence for S instead. Also you don't need to worry about the fact that P and S themselves have types, that won't be important information for you in this level."

Given the opportunity, I would probably change this error message to

argument
  s
is evidence for
  S
but is expected to be evidence for
  P

Or if I can add level specific context into the messages:

argument
  s — “Sybeth's invitation”
is evidence for
  S — “Sybeth is invited to the party”
but the goal requires evidence for
  P — “Pippin is invited to the party”

[kmill]

leanprover/lean4#6891 partially addresses rw