Lean.Compiler.LCNF.FVarUtil

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

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

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

source

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

m Unit

source

instance Lean.Compiler.LCNF.instTraverseFVarExpr :

Lean.Compiler.LCNF.TraverseFVar Lean.Expr

Equations

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

source

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

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

Instances For

source

def Lean.Compiler.LCNF.Arg.forFVarM {m : Type → Type} [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.

Instances For

source

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.

source

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.

Instances For

source

def Lean.Compiler.LCNF.LetValue.forFVarM {m : Type → Type} [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.

Instances For

source

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.

source

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.

Instances For

source

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

Instances For

source

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.

source

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 (Lean.Compiler.LCNF.Param.update param __do_lift)

Instances For

source

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

Instances For

source

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.

source

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

source

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

m Unit

source

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.

source

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.

Instances For

source

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.

Instances For

source

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.

source

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.

source

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.

source

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.

Instances For

source

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

Instances For

source

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.

Instances For

source

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

Instances For

source

def Lean.Compiler.LCNF.anyFVar {α : Type} [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)

Instances For

source

def Lean.Compiler.LCNF.allFVar {α : Type} [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)

Instances For