Def Lean.Parser.Term.Command.quot
Modification history
2022-07-01 15:19
Mathlib/Tactic/CommandQuote.lean
fix: make `(command|...) produce correct type (#297) …
Deleted Lean.Parser.Term.Command.quotView on Github →2021-12-01 10:18
Mathlib/Tactic/CommandQuote.lean
feat: add `` `(command| ..) `` quote (#116)
Added Lean.Parser.Term.Command.quotView on Github →