feat: elaborate opaque command

src/Lean/Elab/Declaration.lean

@@ -57,7 +57,8 @@ private def expandDeclNamespace? (stx : Syntax) : MacroM (Option (Name × Syntax
     if k == ``Lean.Parser.Command.abbrev ||
        k == ``Lean.Parser.Command.def ||
        k == ``Lean.Parser.Command.theorem ||
-       k == ``Lean.Parser.Command.constant ||
+       k == ``Lean.Parser.Command.constant || -- TODO: delete
+       k == ``Lean.Parser.Command.opaque ||
        k == ``Lean.Parser.Command.axiom ||
        k == ``Lean.Parser.Command.inductive ||
        k == ``Lean.Parser.Command.classInductive ||

src/Lean/Elab/DefView.lean

@@ -121,8 +121,8 @@ def mkDefViewOfInstance (modifiers : Modifiers) (stx : Syntax) : CommandElabM De
     declId := declId, binders := binders, type? := type, value := stx[5]
   }
 
-def mkDefViewOfConstant (modifiers : Modifiers) (stx : Syntax) : CommandElabM DefView := do
-  -- leading_parser "constant " >> declId >> declSig >> optional declValSimple
+def mkDefViewOfOpaque (modifiers : Modifiers) (stx : Syntax) : CommandElabM DefView := do
+  -- leading_parser "opaque " >> declId >> declSig >> optional declValSimple
   let (binders, type) := expandDeclSig stx[2]
   let val ← match stx[3].getOptional? with
     | some val => pure val
@@ -144,26 +144,29 @@ def mkDefViewOfExample (modifiers : Modifiers) (stx : Syntax) : DefView :=
 
 def isDefLike (stx : Syntax) : Bool :=
   let declKind := stx.getKind
-  declKind == ``Parser.Command.«abbrev» ||
-  declKind == ``Parser.Command.«def» ||
-  declKind == ``Parser.Command.«theorem» ||
-  declKind == ``Parser.Command.«constant» ||
-  declKind == ``Parser.Command.«instance» ||
-  declKind == ``Parser.Command.«example»
+  declKind == ``Parser.Command.abbrev ||
+  declKind == ``Parser.Command.def ||
+  declKind == ``Parser.Command.theorem ||
+  declKind == ``Parser.Command.constant || -- TODO: delete
+  declKind == ``Parser.Command.opaque ||
+  declKind == ``Parser.Command.instance ||
+  declKind == ``Parser.Command.example
 
 def mkDefView (modifiers : Modifiers) (stx : Syntax) : CommandElabM DefView :=
   let declKind := stx.getKind
   if declKind == ``Parser.Command.«abbrev» then
     return mkDefViewOfAbbrev modifiers stx
-  else if declKind == ``Parser.Command.«def» then
+  else if declKind == ``Parser.Command.def then
     return mkDefViewOfDef modifiers stx
-  else if declKind == ``Parser.Command.«theorem» then
+  else if declKind == ``Parser.Command.theorem then
     return mkDefViewOfTheorem modifiers stx
-  else if declKind == ``Parser.Command.«constant» then
-    mkDefViewOfConstant modifiers stx
-  else if declKind == ``Parser.Command.«instance» then
+  else if declKind == ``Parser.Command.constant then -- TODO: delete
+    mkDefViewOfOpaque modifiers stx
+  else if declKind == ``Parser.Command.opaque then
+    mkDefViewOfOpaque modifiers stx
+  else if declKind == ``Parser.Command.instance then
     mkDefViewOfInstance modifiers stx
-  else if declKind == ``Parser.Command.«example» then
+  else if declKind == ``Parser.Command.example then
     return mkDefViewOfExample modifiers stx
   else
     throwError "unexpected kind of definition"