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

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

Equations

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

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

Equations

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

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} [inst : MonadLiftT Lean.Compiler.LCNF.CompilerM m] [inst : 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.

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

Equations

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

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} [inst : MonadLiftT Lean.Compiler.LCNF.CompilerM m] [inst : 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} [inst : 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} [inst : MonadLiftT Lean.Compiler.LCNF.CompilerM m] [inst : 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 (Lean.Compiler.LCNF.Param.update param __do_lift)

def Lean.Compiler.LCNF.Param.forFVarM {m : Type → Type u_1} [inst : 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} [inst : MonadLiftT Lean.Compiler.LCNF.CompilerM m] [inst : 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} [inst : 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} [inst : MonadLiftT Lean.Compiler.LCNF.CompilerM m] [inst : 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} [inst : 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} [inst : Monad m] [inst : 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} [inst : 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} [inst : Monad m] [inst : 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} [inst : 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} [inst : Lean.Compiler.LCNF.TraverseFVar α] (f : Lean.FVarId → Bool) (x : α) : Bool

Equations

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

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

Equations

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