def Lean.Compiler.LCNF.Code.forEachExpr {ω : Type} {m : Type → Type} [inst : STWorld ω m] [inst : MonadLiftT (ST ω) m] [inst : Monad m] (f : Lean.Expr → m Unit) (c : Lean.Compiler.LCNF.Code) (skipTypes : optParam Bool false) : m Unit

Equations

• Lean.Compiler.LCNF.Code.forEachExpr f c skipTypes = Lean.MonadCacheT.run (Lean.Compiler.LCNF.Code.forEachExpr.visit f skipTypes c)

partial def Lean.Compiler.LCNF.Code.forEachExpr.visit {ω : Type} {m : Type → Type} [inst : STWorld ω m] [inst : MonadLiftT (ST ω) m] [inst : Monad m] (f : Lean.Expr → m Unit) (skipTypes : optParam Bool false) (c : Lean.Compiler.LCNF.Code) : Lean.MonadCacheT Lean.Expr Unit m Unit

def Lean.Compiler.LCNF.Code.forEachExpr.visitParam {ω : Type} {m : Type → Type} [inst : STWorld ω m] [inst : MonadLiftT (ST ω) m] [inst : Monad m] (f : Lean.Expr → m Unit) (skipTypes : optParam Bool false) (p : Lean.Compiler.LCNF.Param) : Lean.MonadCacheT Lean.Expr Unit m Unit

Equations

• Lean.Compiler.LCNF.Code.forEachExpr.visitParam f skipTypes p = Lean.Compiler.LCNF.Code.forEachExpr.visitType f skipTypes p.type

def Lean.Compiler.LCNF.Code.forEachExpr.visitExpr {ω : Type} {m : Type → Type} [inst : STWorld ω m] [inst : MonadLiftT (ST ω) m] [inst : Monad m] (f : Lean.Expr → m Unit) (e : Lean.Expr) : Lean.MonadCacheT Lean.Expr Unit m Unit

Equations

• Lean.Compiler.LCNF.Code.forEachExpr.visitExpr f e = Lean.ForEachExpr.visit (fun e => SeqRight.seqRight (f e) fun x => pure true) e

def Lean.Compiler.LCNF.Code.forEachExpr.visitType {ω : Type} {m : Type → Type} [inst : STWorld ω m] [inst : MonadLiftT (ST ω) m] [inst : Monad m] (f : Lean.Expr → m Unit) (skipTypes : optParam Bool false) (e : Lean.Expr) : Lean.MonadCacheT Lean.Expr Unit m Unit

Equations

• Lean.Compiler.LCNF.Code.forEachExpr.visitType f skipTypes e = if skipTypes = true then pure PUnit.unit else Lean.Compiler.LCNF.Code.forEachExpr.visitExpr f e

def Lean.Compiler.LCNF.Decl.forEachExpr {ω : Type} {m : Type → Type} [inst : STWorld ω m] [inst : MonadLiftT (ST ω) m] [inst : Monad m] (f : Lean.Expr → m Unit) (decl : Lean.Compiler.LCNF.Decl) (skipTypes : optParam Bool false) : m Unit

Equations

• Lean.Compiler.LCNF.Decl.forEachExpr f decl skipTypes = Lean.MonadCacheT.run (Lean.Compiler.LCNF.Decl.forEachExpr.visit f decl skipTypes)

def Lean.Compiler.LCNF.Decl.forEachExpr.visit {ω : Type} {m : Type → Type} [inst : STWorld ω m] [inst : MonadLiftT (ST ω) m] [inst : Monad m] (f : Lean.Expr → m Unit) (decl : Lean.Compiler.LCNF.Decl) (skipTypes : optParam Bool false) : Lean.MonadCacheT Lean.Expr Unit m Unit

Equations

• One or more equations did not get rendered due to their size.