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 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
    instance Lean.Compiler.LCNF.instTraverseFVarExpr :
    TraverseFVar Expr
    Equations
      source
      def Lean.Compiler.LCNF.Arg.mapFVarM {m : Type → Type} [MonadLiftT CompilerM m] [Monad m] (f : FVarId → m FVarId) (arg : Arg) :
      m Arg
      Equations
        Instances For
          source
          def Lean.Compiler.LCNF.Arg.forFVarM {m : Type → Type} [Monad m] (f : FVarId → m Unit) (arg : Arg) :
          m Unit
          Equations
            Instances For
              source
              instance Lean.Compiler.LCNF.instTraverseFVarArg :
              TraverseFVar Arg
              Equations
                source
                def Lean.Compiler.LCNF.LetValue.mapFVarM {m : Type → Type} [MonadLiftT CompilerM m] [Monad m] (f : FVarId → m FVarId) (e : LetValue) :
                m LetValue
                Equations
                  Instances For
                    source
                    def Lean.Compiler.LCNF.LetValue.forFVarM {m : Type → Type} [Monad m] (f : FVarId → m Unit) (e : LetValue) :
                    m Unit
                    Equations
                      Instances For
                        source
                        instance Lean.Compiler.LCNF.instTraverseFVarLetValue :
                        TraverseFVar LetValue
                        Equations
                          source
                          def Lean.Compiler.LCNF.LetDecl.mapFVarM {m : Type → Type} [MonadLiftT CompilerM m] [Monad m] (f : FVarId → m FVarId) (decl : LetDecl) :
                          m LetDecl
                          Equations
                            Instances For
                              source
                              def Lean.Compiler.LCNF.LetDecl.forFVarM {m : Type → Type} [Monad m] (f : FVarId → m Unit) (decl : LetDecl) :
                              m Unit
                              Equations
                                Instances For
                                  source
                                  instance Lean.Compiler.LCNF.instTraverseFVarLetDecl :
                                  TraverseFVar LetDecl
                                  Equations
                                    source
                                    def Lean.Compiler.LCNF.Param.mapFVarM {m : Type → Type u_1} [MonadLiftT CompilerM m] [Monad m] (f : FVarId → m FVarId) (param : Param) :
                                    m Param
                                    Equations
                                      Instances For
                                        source
                                        def Lean.Compiler.LCNF.Param.forFVarM {m : Type → Type u_1} [Monad m] (f : FVarId → m Unit) (param : Param) :
                                        m Unit
                                        Equations
                                          Instances For
                                            source
                                            instance Lean.Compiler.LCNF.instTraverseFVarParam :
                                            TraverseFVar Param
                                            Equations
                                              source
                                              partial def Lean.Compiler.LCNF.Code.mapFVarM {m : Type → Type} [MonadLiftT CompilerM m] [Monad m] (f : FVarId → m FVarId) (c : Code) :
                                              m Code
                                              source
                                              partial def Lean.Compiler.LCNF.Code.forFVarM {m : Type → Type} [Monad m] (f : FVarId → m Unit) (c : Code) :
                                              m Unit
                                              source
                                              instance Lean.Compiler.LCNF.instTraverseFVarCode :
                                              TraverseFVar Code
                                              Equations
                                                source
                                                def Lean.Compiler.LCNF.FunDecl.mapFVarM {m : Type → Type} [MonadLiftT CompilerM m] [Monad m] (f : FVarId → m FVarId) (decl : FunDecl) :
                                                m FunDecl
                                                Equations
                                                  Instances For
                                                    source
                                                    def Lean.Compiler.LCNF.FunDecl.forFVarM {m : Type → Type} [Monad m] (f : FVarId → m Unit) (decl : FunDecl) :
                                                    m Unit
                                                    Equations
                                                      Instances For
                                                        source
                                                        instance Lean.Compiler.LCNF.instTraverseFVarFunDecl :
                                                        TraverseFVar FunDecl
                                                        Equations
                                                          source
                                                          instance Lean.Compiler.LCNF.instTraverseFVarCodeDecl :
                                                          TraverseFVar CodeDecl
                                                          Equations
                                                            source
                                                            instance Lean.Compiler.LCNF.instTraverseFVarAlt :
                                                            TraverseFVar Alt
                                                            Equations
                                                              source
                                                              def Lean.Compiler.LCNF.anyFVarM {m : Type → Type} {α : Type} [Monad m] [TraverseFVar α] (f : FVarId → m Bool) (x : α) :
                                                              m Bool
                                                              Equations
                                                                Instances For
                                                                  source
                                                                  def Lean.Compiler.LCNF.anyFVarM.go {m : Type → Type} [Monad m] (f : FVarId → m Bool) (fvar : FVarId) :
                                                                  OptionT m Unit
                                                                  Equations
                                                                    Instances For
                                                                      source
                                                                      def Lean.Compiler.LCNF.allFVarM {m : Type → Type} {α : Type} [Monad m] [TraverseFVar α] (f : FVarId → m Bool) (x : α) :
                                                                      m Bool
                                                                      Equations
                                                                        Instances For
                                                                          source
                                                                          def Lean.Compiler.LCNF.allFVarM.go {m : Type → Type} [Monad m] (f : FVarId → m Bool) (fvar : FVarId) :
                                                                          OptionT m Unit
                                                                          Equations
                                                                            Instances For
                                                                              source
                                                                              def Lean.Compiler.LCNF.anyFVar {α : Type} [TraverseFVar α] (f : FVarId → Bool) (x : α) :
                                                                              Bool
                                                                              Equations
                                                                                Instances For
                                                                                  source
                                                                                  def Lean.Compiler.LCNF.allFVar {α : Type} [TraverseFVar α] (f : FVarId → Bool) (x : α) :
                                                                                  Bool
                                                                                  Equations
                                                                                    Instances For