a3226d4fe4
When editing core Lean, the `pp.proofs` feature causes goal states to fail to display in the Infoview, instead showing only "error when printing message: unknown constant '«term⋯»'". This PR moves the `⋯` syntax from Init.NotationExtra to Lean.Elab.BuiltinTerm It also makes it so that `⋯` elaborates as `_` while logging a warning, rather than throwing an error, which should be somewhat more friendly when copy/pasting from the Infoview. Closes #3476 |
||
|---|---|---|
| .. | ||
| Delaborator | ||
| Basic.lean | ||
| Delaborator.lean | ||
| Formatter.lean | ||
| Parenthesizer.lean | ||