Lean.Compiler.LCNF.FVarUtil

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

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

Instances

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

source

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

m Unit

source

@[implicit_reducible]

instance Lean.Compiler.LCNF.instTraverseFVarExpr :

TraverseFVar Expr

source

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)

Instances For

source

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

m Unit

Instances For

source

@[implicit_reducible]

instance Lean.Compiler.LCNF.instTraverseFVarArg {pu : Purity} :

TraverseFVar (Arg pu)

source

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)

Instances For

source

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

m Unit

Instances For

source

@[implicit_reducible]

instance Lean.Compiler.LCNF.instTraverseFVarLetValue {pu : Purity} :

TraverseFVar (LetValue pu)

source

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)

Instances For

source

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

m Unit

Instances For

source

@[implicit_reducible]

instance Lean.Compiler.LCNF.instTraverseFVarLetDecl {pu : Purity} :

TraverseFVar (LetDecl pu)

source

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)

Instances For

source

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

m Unit

Instances For

source

@[implicit_reducible]

instance Lean.Compiler.LCNF.instTraverseFVarParam {pu : Purity} :

TraverseFVar (Param pu)

source

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)

source

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

m Unit

source

@[implicit_reducible]

instance Lean.Compiler.LCNF.instTraverseFVarCode {pu : Purity} :

TraverseFVar (Code pu)

source

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)

Instances For

source

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

m Unit

Instances For

source

@[implicit_reducible]

instance Lean.Compiler.LCNF.instTraverseFVarFunDecl {pu : Purity} :

TraverseFVar (FunDecl pu)

source

@[implicit_reducible]

instance Lean.Compiler.LCNF.instTraverseFVarCodeDecl {pu : Purity} :

TraverseFVar (CodeDecl pu)

source

@[implicit_reducible]

instance Lean.Compiler.LCNF.instTraverseFVarAlt {pu : Purity} :

TraverseFVar (Alt pu)

source

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

m Bool

Instances For

source

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

m Bool

Instances For

source

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

Bool

Instances For

source

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

Bool

Instances For