lean4-htt/src/Lean/PrettyPrinter/Delaborator
Leonardo de Moura 1c1e6d79a7 feat: add equality proof for named patterns
The user can optionally name the equality proof.
The new test demostrates how to name the equality proof.

closes #501
2022-01-18 12:43:01 -08:00
..
Basic.lean chore: remove arbitrary 2022-01-15 12:14:27 -08:00
Builtins.lean feat: add equality proof for named patterns 2022-01-18 12:43:01 -08:00
Options.lean chore: apply suggestions from code review 2022-01-03 13:43:33 +01:00
SubExpr.lean doc: add review comments 2021-08-24 08:57:41 -07:00
TopDownAnalyze.lean chore: fix codebase 2021-12-10 13:12:09 -08:00