Commit 2021-12-01 10:18 d3cb87d0

View on Github →

feat: add `(command| ..) quote (#116)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Tactic/CommandQuote.lean

added def Lean.Elab.Term.elabCommandQuot

added def Lean.Parser.Term.Command.quot