Documentation

Lean.Meta.Transform

def Lean.Core.transform {m : TypeType} [inst : Monad m] [inst : MonadLiftT Lean.CoreM m] [inst : MonadControlT Lean.CoreM m] (input : Lean.Expr) (pre : optParam (Lean.Exprm Lean.TransformStep) fun e => pure (Lean.TransformStep.visit e)) (post : optParam (Lean.Exprm Lean.TransformStep) fun e => pure (Lean.TransformStep.done e)) :
Equations
def Lean.Meta.transform {m : TypeType} [inst : Monad m] [inst : MonadLiftT Lean.MetaM m] [inst : MonadControlT Lean.MetaM m] (input : Lean.Expr) (pre : optParam (Lean.Exprm Lean.TransformStep) fun e => pure (Lean.TransformStep.visit e)) (post : optParam (Lean.Exprm Lean.TransformStep) fun e => pure (Lean.TransformStep.done e)) :
Equations
Equations