Def Lean.Elab.Term.elabCommandQuot

Modification history

2022-11-15 08:49
Mathlib/Tactic/CommandQuote.lean
chore: remove obsolete CommandQuote (#602)
Deleted Lean.Elab.Term.elabCommandQuotView on Github →
2022-10-20 15:23
Mathlib/Tactic/CommandQuote.lean
chore: update lean + std4 10-20 (#483)
Modified Lean.Elab.Term.elabCommandQuotView on Github →
2022-07-04 10:05
Mathlib/Tactic/CommandQuote.lean
fix: command quotation (#299)
Added Lean.Elab.Term.elabCommandQuotView on Github →
2022-07-01 15:19
Mathlib/Tactic/CommandQuote.lean
fix: make `(command|...) produce correct type (#297) …
Deleted Lean.Elab.Term.elabCommandQuotView on Github →
2021-12-01 10:18
Mathlib/Tactic/CommandQuote.lean
feat: add `` `(command| ..) `` quote (#116)
Added Lean.Elab.Term.elabCommandQuotView on Github →
2021-11-30 14:25
Mathlib/Mathport/Syntax.lean
chore: move run_cmd to separate file and remove comments (#111)
Deleted Lean.Elab.Term.elabCommandQuotView on Github →
2021-11-08 09:32
Mathlib/Mathport/Syntax.lean
refactor(Mathport): move mathport prelude to mathlib4 (#80) …
Added Lean.Elab.Term.elabCommandQuotView on Github →