Documentation

Lean.Meta.Reduce

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

Lean.MetaM Lean.Expr

Equations

Lean.Meta.reduce e explicitOnly skipTypes skipProofs = (fun visit => Lean.MonadCacheT.run (visit e)) (Lean.Meta.reduce.visit explicitOnly skipTypes skipProofs)

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

Lean.MonadCacheT Lean.Expr Lean.Expr Lean.MetaM Lean.Expr