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

@[implicit_reducible]

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} {pu : Purity} [MonadLiftT CompilerM m] [Monad m] (f : FVarId → m FVarId) (arg : Arg pu) : m (Arg pu)

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 h) = do let __do_lift ← Lean.Compiler.LCNF.mapFVarM f e pure ((Lean.Compiler.LCNF.Arg.type e h).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} {pu : Purity} [Monad m] (f : FVarId → m Unit) (arg : Arg pu) : 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 h) = Lean.Compiler.LCNF.forFVarM f e
• Lean.Compiler.LCNF.Arg.forFVarM f (Lean.Compiler.LCNF.Arg.fvar fvarId) = f fvarId

@[implicit_reducible]

instance Lean.Compiler.LCNF.instTraverseFVarArg {pu : Purity} : TraverseFVar (Arg pu)

Equations

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

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

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
• Lean.Compiler.LCNF.LetValue.mapFVarM f (Lean.Compiler.LCNF.LetValue.oproj i fvarId h) = do let __do_lift ← f fvarId pure ((Lean.Compiler.LCNF.LetValue.oproj i fvarId h).updateProj! __do_lift)
• Lean.Compiler.LCNF.LetValue.mapFVarM f (Lean.Compiler.LCNF.LetValue.uproj i fvarId h) = do let __do_lift ← f fvarId pure ((Lean.Compiler.LCNF.LetValue.uproj i fvarId h).updateProj! __do_lift)
• Lean.Compiler.LCNF.LetValue.mapFVarM f (Lean.Compiler.LCNF.LetValue.reset n fvarId h) = do let __do_lift ← f fvarId pure ((Lean.Compiler.LCNF.LetValue.reset n fvarId h).updateReset! n __do_lift)
• Lean.Compiler.LCNF.LetValue.mapFVarM f (Lean.Compiler.LCNF.LetValue.box ty fvarId h) = do let __do_lift ← f fvarId pure ((Lean.Compiler.LCNF.LetValue.box ty fvarId h).updateBox! ty __do_lift)
• Lean.Compiler.LCNF.LetValue.mapFVarM f (Lean.Compiler.LCNF.LetValue.unbox fvarId h) = do let __do_lift ← f fvarId pure ((Lean.Compiler.LCNF.LetValue.unbox fvarId h).updateUnbox! __do_lift)

def Lean.Compiler.LCNF.LetValue.forFVarM {m : Type → Type} {pu : Purity} [Monad m] (f : FVarId → m Unit) (e : LetValue pu) : 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 h) = f fvarId
• Lean.Compiler.LCNF.LetValue.forFVarM f (Lean.Compiler.LCNF.LetValue.oproj i fvarId h) = f fvarId
• Lean.Compiler.LCNF.LetValue.forFVarM f (Lean.Compiler.LCNF.LetValue.sproj n offset fvarId h) = f fvarId
• Lean.Compiler.LCNF.LetValue.forFVarM f (Lean.Compiler.LCNF.LetValue.uproj i fvarId h) = f fvarId
• Lean.Compiler.LCNF.LetValue.forFVarM f (Lean.Compiler.LCNF.LetValue.reset n fvarId h) = f fvarId
• Lean.Compiler.LCNF.LetValue.forFVarM f (Lean.Compiler.LCNF.LetValue.box ty fvarId h) = f fvarId
• Lean.Compiler.LCNF.LetValue.forFVarM f (Lean.Compiler.LCNF.LetValue.unbox fvarId h) = f fvarId
• Lean.Compiler.LCNF.LetValue.forFVarM f (Lean.Compiler.LCNF.LetValue.const declName us args h) = Array.forM (Lean.Compiler.LCNF.forFVarM f) args
• Lean.Compiler.LCNF.LetValue.forFVarM f (Lean.Compiler.LCNF.LetValue.pap fn args h) = Array.forM (Lean.Compiler.LCNF.forFVarM f) args
• Lean.Compiler.LCNF.LetValue.forFVarM f (Lean.Compiler.LCNF.LetValue.fap fn args h) = Array.forM (Lean.Compiler.LCNF.forFVarM f) args
• Lean.Compiler.LCNF.LetValue.forFVarM f (Lean.Compiler.LCNF.LetValue.ctor i args h) = 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
• Lean.Compiler.LCNF.LetValue.forFVarM f (Lean.Compiler.LCNF.LetValue.reuse fvarId i updateHeader args h) = do f fvarId Array.forM (Lean.Compiler.LCNF.forFVarM f) args

@[implicit_reducible]

instance Lean.Compiler.LCNF.instTraverseFVarLetValue {pu : Purity} : TraverseFVar (LetValue pu)

Equations

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

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

Equations

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

def Lean.Compiler.LCNF.LetDecl.forFVarM {m : Type → Type} {pu : Purity} [Monad m] (f : FVarId → m Unit) (decl : LetDecl pu) : 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

@[implicit_reducible]

instance Lean.Compiler.LCNF.instTraverseFVarLetDecl {pu : Purity} : TraverseFVar (LetDecl pu)

Equations

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

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

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} {pu : Purity} [Monad m] (f : FVarId → m Unit) (param : Param pu) : m Unit

Equations

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

@[implicit_reducible]

instance Lean.Compiler.LCNF.instTraverseFVarParam {pu : Purity} : TraverseFVar (Param pu)

Equations

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

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

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

@[implicit_reducible]

instance Lean.Compiler.LCNF.instTraverseFVarCode {pu : Purity} : TraverseFVar (Code pu)

Equations

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

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

Equations

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

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

Equations

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

@[implicit_reducible]

instance Lean.Compiler.LCNF.instTraverseFVarFunDecl {pu : Purity} : TraverseFVar (FunDecl pu)

Equations

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

@[implicit_reducible]

instance Lean.Compiler.LCNF.instTraverseFVarCodeDecl {pu : Purity} : TraverseFVar (CodeDecl pu)

Equations

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

@[implicit_reducible]

instance Lean.Compiler.LCNF.instTraverseFVarAlt {pu : Purity} : TraverseFVar (Alt pu)

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.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.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