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

Equations

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

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

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

Equations

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