Check type of a name

Stream: metaprogramming / tactics

[Thomas Murrills]

Is there an existing way to spell evalConstCheck without the eval? Basically

def constCheck (env : Environment) (constName typeName : Name) : Bool :=
  match env.find? constName with
    | none      => throw ("unknown constant '" ++ toString constName ++ "'")
    | some info =>
      match info.type with
      | Expr.const c _ => c == typeName
      | _ => throw "not a constant"

I feel like this is a really common function, and I'm just drawing a blank on the name...!

[Alex J. Best]

docs4#Lean.getConstInfo and then .type maybe? Edit oops didn't realise this was a months old post sorry