Documentation

Lean.Meta.GetConst

def Lean.Meta.canUnfold (info : Lean.ConstantInfo) :

Lean.MetaM Bool

Equations

Lean.Meta.canUnfold info = do let ctx ← read match ctx.canUnfold? with | some f => liftM (f ctx.config info) | x => liftM (Lean.Meta.canUnfoldDefault ctx.config info)

def Lean.Meta.getConst? (constName : Lean.Name) :

Lean.MetaM (Option Lean.ConstantInfo)

Equations

Lean.Meta.getConst? constName = do let env ← Lean.getEnv match Lean.Environment.find? env constName with | some info@h:(Lean.ConstantInfo.thmInfo x) => Lean.Meta.getTheoremInfo info | some info@h:(Lean.ConstantInfo.defnInfo x) => do let a ← Lean.Meta.canUnfold info if a = true then pure (some info) else pure none | some info => pure (some info) | none => Lean.throwUnknownConstant constName

def Lean.Meta.getConstNoEx? (constName : Lean.Name) :

Lean.MetaM (Option Lean.ConstantInfo)

Equations

Lean.Meta.getConstNoEx? constName = do let env ← Lean.getEnv match Lean.Environment.find? env constName with | some info@h:(Lean.ConstantInfo.thmInfo x) => Lean.Meta.getTheoremInfo info | some info@h:(Lean.ConstantInfo.defnInfo x) => do let a ← Lean.Meta.canUnfold info if a = true then pure (some info) else pure none | some info => pure (some info) | none => pure none