Lean4
/-- `getId stx` takes as input a `Syntax` `stx`.
If `stx` contains a `declId`, then it returns the `ident`-syntax for the `declId`.
If `stx` is a nameless instance, then it also tries to fetch the `ident` for the instance.
Otherwise it returns `.missing`. -/
def getId (stx : Syntax) : CommandElabM Syntax := do
-- If the command contains a `declId`, we use the implied `ident`.
match stx.find? (·.isOfKind ``Lean.Parser.Command.declId) with
| some declId =>
return declId[0]
| none =>
-- Otherwise, the command could be a nameless `instance`.
match stx.find? (·.isOfKind ``Lean.Parser.Command.instance) with
| none =>
return .missing
| some stx =>
do
-- if it is a nameless `instance`, we retrieve the autogenerated name
let dv ← mkDefViewOfInstance { } stx
return dv.declId[0]
