Documentation

Lean.Compiler.LCNF.FVarUtil

source
class Lean.Compiler.LCNF.TraverseFVar (α : Type) :
Type 1
Instances
    source
    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
    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
    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
      Instances For
        source
        instance Lean.Compiler.LCNF.instTraverseFVarArg :
        Lean.Compiler.LCNF.TraverseFVar Lean.Compiler.LCNF.Arg
        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
        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
          Instances For
            source
            instance Lean.Compiler.LCNF.instTraverseFVarLetValue :
            Lean.Compiler.LCNF.TraverseFVar Lean.Compiler.LCNF.LetValue
            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
            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
              Instances For
                source
                instance Lean.Compiler.LCNF.instTraverseFVarLetDecl :
                Lean.Compiler.LCNF.TraverseFVar Lean.Compiler.LCNF.LetDecl
                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
                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
                  Instances For
                    source
                    instance Lean.Compiler.LCNF.instTraverseFVarParam :
                    Lean.Compiler.LCNF.TraverseFVar Lean.Compiler.LCNF.Param
                    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
                    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
                    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
                      Instances For
                        source
                        instance Lean.Compiler.LCNF.instTraverseFVarFunDecl :
                        Lean.Compiler.LCNF.TraverseFVar Lean.Compiler.LCNF.FunDecl
                        source
                        instance Lean.Compiler.LCNF.instTraverseFVarCodeDecl :
                        Lean.Compiler.LCNF.TraverseFVar Lean.Compiler.LCNF.CodeDecl
                        source
                        instance Lean.Compiler.LCNF.instTraverseFVarAlt :
                        Lean.Compiler.LCNF.TraverseFVar Lean.Compiler.LCNF.Alt
                        source
                        def Lean.Compiler.LCNF.anyFVarM {m : Type → Type} {α : Type} [Monad m] [Lean.Compiler.LCNF.TraverseFVar α] (f : Lean.FVarId → m Bool) (x : α) :
                        m Bool
                        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
                          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
                            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
                              Instances For
                                source
                                def Lean.Compiler.LCNF.anyFVar {α : Type} [Lean.Compiler.LCNF.TraverseFVar α] (f : Lean.FVarId → Bool) (x : α) :
                                Bool
                                Instances For
                                  source
                                  def Lean.Compiler.LCNF.allFVar {α : Type} [Lean.Compiler.LCNF.TraverseFVar α] (f : Lean.FVarId → Bool) (x : α) :
                                  Bool
                                  Instances For