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

• mapFVarM : {m : Type → Type} → [inst : MonadLiftT Lean.Compiler.LCNF.CompilerM m] → [inst : Monad m] → (Lean.FVarId → m Lean.FVarId) → α → m α
• forFVarM : {m : Type → Type} → [inst : Monad m] → (Lean.FVarId → m Unit) → α → m Unit

Instances

• Lean.Compiler.LCNF.instTraverseFVarAlt
• Lean.Compiler.LCNF.instTraverseFVarArg
• Lean.Compiler.LCNF.instTraverseFVarCode
• Lean.Compiler.LCNF.instTraverseFVarCodeDecl
• Lean.Compiler.LCNF.instTraverseFVarExpr
• Lean.Compiler.LCNF.instTraverseFVarFunDecl
• Lean.Compiler.LCNF.instTraverseFVarLetDecl
• Lean.Compiler.LCNF.instTraverseFVarLetValue
• Lean.Compiler.LCNF.instTraverseFVarParam

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

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

instance Lean.Compiler.LCNF.instTraverseFVarExpr : Lean.Compiler.LCNF.TraverseFVar Lean.Expr

Equations

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

def Lean.Compiler.LCNF.Arg.mapFVarM {m : Type → Type} [MonadLiftT Lean.Compiler.LCNF.CompilerM m] [Monad m] (f : Lean.FVarId → m Lean.FVarId) (arg : Lean.Compiler.LCNF.Arg) : m Lean.Compiler.LCNF.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 : Lean.FVarId → m Unit) (arg : Lean.Compiler.LCNF.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 : Lean.Compiler.LCNF.TraverseFVar Lean.Compiler.LCNF.Arg

Equations

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

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

Equations

• One or more equations did not get rendered due to their size.
• Lean.Compiler.LCNF.LetValue.mapFVarM f (Lean.Compiler.LCNF.LetValue.value value) = pure (Lean.Compiler.LCNF.LetValue.value 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 : Lean.FVarId → m Unit) (e : Lean.Compiler.LCNF.LetValue) : m Unit

Equations

• Lean.Compiler.LCNF.LetValue.forFVarM f (Lean.Compiler.LCNF.LetValue.value 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 : Lean.Compiler.LCNF.TraverseFVar Lean.Compiler.LCNF.LetValue

Equations

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

def Lean.Compiler.LCNF.LetDecl.mapFVarM {m : Type → Type} [MonadLiftT Lean.Compiler.LCNF.CompilerM m] [Monad m] (f : Lean.FVarId → m Lean.FVarId) (decl : Lean.Compiler.LCNF.LetDecl) : m Lean.Compiler.LCNF.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 : Lean.FVarId → m Unit) (decl : Lean.Compiler.LCNF.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 : Lean.Compiler.LCNF.TraverseFVar Lean.Compiler.LCNF.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 Lean.Compiler.LCNF.CompilerM m] [Monad m] (f : Lean.FVarId → m Lean.FVarId) (param : Lean.Compiler.LCNF.Param) : m Lean.Compiler.LCNF.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 : Lean.FVarId → m Unit) (param : Lean.Compiler.LCNF.Param) : m Unit

Equations

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

instance Lean.Compiler.LCNF.instTraverseFVarParam : Lean.Compiler.LCNF.TraverseFVar Lean.Compiler.LCNF.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 Lean.Compiler.LCNF.CompilerM m] [Monad m] (f : Lean.FVarId → m Lean.FVarId) (c : Lean.Compiler.LCNF.Code) : m Lean.Compiler.LCNF.Code

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

instance Lean.Compiler.LCNF.instTraverseFVarCode : Lean.Compiler.LCNF.TraverseFVar Lean.Compiler.LCNF.Code

Equations

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

def Lean.Compiler.LCNF.FunDecl.mapFVarM {m : Type → Type} [MonadLiftT Lean.Compiler.LCNF.CompilerM m] [Monad m] (f : Lean.FVarId → m Lean.FVarId) (decl : Lean.Compiler.LCNF.FunDecl) : m Lean.Compiler.LCNF.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 : Lean.FVarId → m Unit) (decl : Lean.Compiler.LCNF.FunDecl) : m Unit

Equations

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

instance Lean.Compiler.LCNF.instTraverseFVarFunDecl : Lean.Compiler.LCNF.TraverseFVar Lean.Compiler.LCNF.FunDecl

Equations

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

instance Lean.Compiler.LCNF.instTraverseFVarCodeDecl : Lean.Compiler.LCNF.TraverseFVar Lean.Compiler.LCNF.CodeDecl

Equations

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

instance Lean.Compiler.LCNF.instTraverseFVarAlt : Lean.Compiler.LCNF.TraverseFVar Lean.Compiler.LCNF.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] [Lean.Compiler.LCNF.TraverseFVar α] (f : Lean.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 : Lean.FVarId → m Bool) (fvar : Lean.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] [Lean.Compiler.LCNF.TraverseFVar α] (f : Lean.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 : Lean.FVarId → m Bool) (fvar : Lean.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} [Lean.Compiler.LCNF.TraverseFVar α] (f : Lean.FVarId → Bool) (x : α) : Bool

Equations

• Lean.Compiler.LCNF.anyFVar f x = (Lean.Compiler.LCNF.anyFVarM f x).run

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

Equations

• Lean.Compiler.LCNF.allFVar f x = (Lean.Compiler.LCNF.allFVarM f x).run