class Lean.Compiler.LCNF.TraverseFVar (α : Type) : Type 1

• mapFVarM {m : Type → Type} [MonadLiftT CompilerM m] [Monad m] (f : FVarId → m FVarId) (val : α) : m α
• forFVarM {m : Type → Type} [Monad m] (f : FVarId → m Unit) (val : α) : m Unit

partial def Lean.Compiler.LCNF.Expr.mapFVarM {m : Type → Type u_1} [MonadLiftT CompilerM m] [Monad m] (f : FVarId → m FVarId) (e : Expr) : m Expr

partial def Lean.Compiler.LCNF.Expr.forFVarM {m : Type → Type u_1} [Monad m] (f : FVarId → m Unit) (e : Expr) : m Unit

instance Lean.Compiler.LCNF.instTraverseFVarExpr : TraverseFVar Expr

Equations

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

def Lean.Compiler.LCNF.Arg.mapFVarM {m : Type → Type} [MonadLiftT CompilerM m] [Monad m] (f : FVarId → m FVarId) (arg : Arg) : m Arg

Equations

• Lean.Compiler.LCNF.Arg.mapFVarM f Lean.Compiler.LCNF.Arg.erased = pure Lean.Compiler.LCNF.Arg.erased
• Lean.Compiler.LCNF.Arg.mapFVarM f (Lean.Compiler.LCNF.Arg.type e) = do let __do_lift ← Lean.Compiler.LCNF.mapFVarM f e pure ((Lean.Compiler.LCNF.Arg.type e).updateType! __do_lift)
• Lean.Compiler.LCNF.Arg.mapFVarM f (Lean.Compiler.LCNF.Arg.fvar fvarId) = do let __do_lift ← f fvarId pure ((Lean.Compiler.LCNF.Arg.fvar fvarId).updateFVar! __do_lift)

def Lean.Compiler.LCNF.Arg.forFVarM {m : Type → Type} [Monad m] (f : FVarId → m Unit) (arg : Arg) : m Unit

Equations

• Lean.Compiler.LCNF.Arg.forFVarM f Lean.Compiler.LCNF.Arg.erased = pure ()
• Lean.Compiler.LCNF.Arg.forFVarM f (Lean.Compiler.LCNF.Arg.type e) = Lean.Compiler.LCNF.forFVarM f e
• Lean.Compiler.LCNF.Arg.forFVarM f (Lean.Compiler.LCNF.Arg.fvar fvarId) = f fvarId

instance Lean.Compiler.LCNF.instTraverseFVarArg : TraverseFVar Arg

Equations

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

def Lean.Compiler.LCNF.LetValue.mapFVarM {m : Type → Type} [MonadLiftT CompilerM m] [Monad m] (f : FVarId → m FVarId) (e : LetValue) : m LetValue

Equations

• One or more equations did not get rendered due to their size.
• Lean.Compiler.LCNF.LetValue.mapFVarM f (Lean.Compiler.LCNF.LetValue.lit value) = pure (Lean.Compiler.LCNF.LetValue.lit value)
• Lean.Compiler.LCNF.LetValue.mapFVarM f Lean.Compiler.LCNF.LetValue.erased = pure Lean.Compiler.LCNF.LetValue.erased

def Lean.Compiler.LCNF.LetValue.forFVarM {m : Type → Type} [Monad m] (f : FVarId → m Unit) (e : LetValue) : m Unit

Equations

• Lean.Compiler.LCNF.LetValue.forFVarM f (Lean.Compiler.LCNF.LetValue.lit value) = pure ()
• Lean.Compiler.LCNF.LetValue.forFVarM f Lean.Compiler.LCNF.LetValue.erased = pure ()
• Lean.Compiler.LCNF.LetValue.forFVarM f (Lean.Compiler.LCNF.LetValue.proj typeName idx fvarId) = f fvarId
• Lean.Compiler.LCNF.LetValue.forFVarM f (Lean.Compiler.LCNF.LetValue.const declName us args) = Array.forM (Lean.Compiler.LCNF.forFVarM f) args
• Lean.Compiler.LCNF.LetValue.forFVarM f (Lean.Compiler.LCNF.LetValue.fvar fvarId args) = do f fvarId Array.forM (Lean.Compiler.LCNF.forFVarM f) args

instance Lean.Compiler.LCNF.instTraverseFVarLetValue : TraverseFVar LetValue

Equations

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

def Lean.Compiler.LCNF.LetDecl.mapFVarM {m : Type → Type} [MonadLiftT CompilerM m] [Monad m] (f : FVarId → m FVarId) (decl : LetDecl) : m LetDecl

Equations

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

def Lean.Compiler.LCNF.LetDecl.forFVarM {m : Type → Type} [Monad m] (f : FVarId → m Unit) (decl : LetDecl) : m Unit

Equations

• Lean.Compiler.LCNF.LetDecl.forFVarM f decl = do Lean.Compiler.LCNF.Expr.forFVarM f decl.type Lean.Compiler.LCNF.LetValue.forFVarM f decl.value

instance Lean.Compiler.LCNF.instTraverseFVarLetDecl : TraverseFVar LetDecl

Equations

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

def Lean.Compiler.LCNF.Param.mapFVarM {m : Type → Type u_1} [MonadLiftT CompilerM m] [Monad m] (f : FVarId → m FVarId) (param : Param) : m Param

Equations

• Lean.Compiler.LCNF.Param.mapFVarM f param = do let __do_lift ← Lean.Compiler.LCNF.Expr.mapFVarM f param.type liftM (param.update __do_lift)

def Lean.Compiler.LCNF.Param.forFVarM {m : Type → Type u_1} [Monad m] (f : FVarId → m Unit) (param : Param) : m Unit

Equations

• Lean.Compiler.LCNF.Param.forFVarM f param = Lean.Compiler.LCNF.Expr.forFVarM f param.type

instance Lean.Compiler.LCNF.instTraverseFVarParam : TraverseFVar Param

Equations

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

partial def Lean.Compiler.LCNF.Code.mapFVarM {m : Type → Type} [MonadLiftT CompilerM m] [Monad m] (f : FVarId → m FVarId) (c : Code) : m Code

partial def Lean.Compiler.LCNF.Code.forFVarM {m : Type → Type} [Monad m] (f : FVarId → m Unit) (c : Code) : m Unit

instance Lean.Compiler.LCNF.instTraverseFVarCode : TraverseFVar Code

Equations

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

def Lean.Compiler.LCNF.FunDecl.mapFVarM {m : Type → Type} [MonadLiftT CompilerM m] [Monad m] (f : FVarId → m FVarId) (decl : FunDecl) : m FunDecl

Equations

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

def Lean.Compiler.LCNF.FunDecl.forFVarM {m : Type → Type} [Monad m] (f : FVarId → m Unit) (decl : FunDecl) : m Unit

Equations

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

instance Lean.Compiler.LCNF.instTraverseFVarFunDecl : TraverseFVar FunDecl

Equations

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

instance Lean.Compiler.LCNF.instTraverseFVarCodeDecl : TraverseFVar CodeDecl

Equations

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

instance Lean.Compiler.LCNF.instTraverseFVarAlt : TraverseFVar Alt

Equations

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

def Lean.Compiler.LCNF.anyFVarM {m : Type → Type} {α : Type} [Monad m] [TraverseFVar α] (f : FVarId → m Bool) (x : α) : m Bool

Equations

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

def Lean.Compiler.LCNF.anyFVarM.go {m : Type → Type} [Monad m] (f : FVarId → m Bool) (fvar : FVarId) : OptionT m Unit

Equations

• Lean.Compiler.LCNF.anyFVarM.go f fvar = do let __do_lift ← liftM (f fvar) if __do_lift = true then failure else pure PUnit.unit

def Lean.Compiler.LCNF.allFVarM {m : Type → Type} {α : Type} [Monad m] [TraverseFVar α] (f : FVarId → m Bool) (x : α) : m Bool

Equations

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

def Lean.Compiler.LCNF.allFVarM.go {m : Type → Type} [Monad m] (f : FVarId → m Bool) (fvar : FVarId) : OptionT m Unit

Equations

• Lean.Compiler.LCNF.allFVarM.go f fvar = do let __do_lift ← liftM (f fvar) if (!__do_lift) = true then failure else pure PUnit.unit

def Lean.Compiler.LCNF.anyFVar {α : Type} [TraverseFVar α] (f : FVarId → Bool) (x : α) : Bool

Equations

• Lean.Compiler.LCNF.anyFVar f x = (Lean.Compiler.LCNF.anyFVarM (fun (x : Lean.FVarId) => pure (f x)) x).run

def Lean.Compiler.LCNF.allFVar {α : Type} [TraverseFVar α] (f : FVarId → Bool) (x : α) : Bool

Equations

• Lean.Compiler.LCNF.allFVar f x = (Lean.Compiler.LCNF.allFVarM (fun (x : Lean.FVarId) => pure (f x)) x).run