def getTypeM (name : Lean.Name) : Lean.MetaM (Option Lean.Format)

Equations

• getTypeM name = do let env ← Lean.getEnv Option.mapM (fun (d : Lean.ConstantInfo) => Lean.Meta.ppExpr d.type) (env.find? name)

def getTypeCore (name : Lean.Name) : Lean.CoreM (Option Lean.Format)

Equations

• getTypeCore name = (getTypeM name).run'

def getProofM (name : Lean.Name) : Lean.MetaM (Option Lean.Format)

Equations

• One or more equations did not get rendered due to their size.