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

Mathlib.lean

@@ -39,6 +39,7 @@ import Mathlib.Mathport.Syntax
 import Mathlib.Tactic.Basic
 import Mathlib.Tactic.Cache
 import Mathlib.Tactic.Coe
+import Mathlib.Tactic.CommandQuote
 import Mathlib.Tactic.Core
 import Mathlib.Tactic.Ext
 import Mathlib.Tactic.Find

Mathlib/Tactic/CommandQuote.lean

@@ -0,0 +1,14 @@
+/-
+Copyright (c) 2021 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mario Carneiro
+-/
+import Lean
+
+namespace Lean
+
+@[termParser default+1] def Parser.Term.Command.quot : Parser :=
+  leading_parser "`(command|" >> incQuotDepth commandParser >> ")"
+
+@[termElab Command.quot] def Elab.Term.elabCommandQuot : TermElab :=
+  adaptExpander Quotation.stxQuot.expand