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

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

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

Lean.MetaM (Option Lean.ConstantInfo)

Equations

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