Documentation

Lean.Compiler.LCNF.Renaming

source
@[reducible, inline]
abbrev Lean.Compiler.LCNF.Renaming :
Type

A mapping from free variable id to binder name.

Equations
    Instances For
      source
      def Lean.Compiler.LCNF.Param.applyRenaming (param : Param) (r : Renaming) :
      CompilerM Param
      Equations
        Instances For
          source
          def Lean.Compiler.LCNF.LetDecl.applyRenaming (decl : LetDecl) (r : Renaming) :
          CompilerM LetDecl
          Equations
            Instances For
              source
              partial def Lean.Compiler.LCNF.FunDecl.applyRenaming (decl : FunDecl) (r : Renaming) :
              CompilerM FunDecl
              source
              partial def Lean.Compiler.LCNF.Code.applyRenaming (code : Code) (r : Renaming) :
              CompilerM Code
              source
              def Lean.Compiler.LCNF.Decl.applyRenaming (decl : Decl) (r : Renaming) :
              CompilerM Decl
              Equations
                Instances For