← Mathematical handbook

def Lean.Meta.reduce (e : Expr) (explicitOnly skipTypes skipProofs : Bool := true) : MetaM Expr

Equations

• Lean.Meta.reduce e explicitOnly skipTypes skipProofs = (Lean.Meta.reduce.visit✝ explicitOnly skipTypes skipProofs e).run

def Lean.Meta.reduceAll (e : Expr) : MetaM Expr

Equations

• Lean.Meta.reduceAll e = Lean.Meta.reduce e false false false