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

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

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