HepLean 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 : Lean.Compiler.LCNF.Param) (r : Lean.Compiler.LCNF.Renaming) :
    Lean.Compiler.LCNF.CompilerM Lean.Compiler.LCNF.Param
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def Lean.Compiler.LCNF.LetDecl.applyRenaming (decl : Lean.Compiler.LCNF.LetDecl) (r : Lean.Compiler.LCNF.Renaming) :
      Lean.Compiler.LCNF.CompilerM Lean.Compiler.LCNF.LetDecl
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        partial def Lean.Compiler.LCNF.FunDeclCore.applyRenaming (decl : Lean.Compiler.LCNF.FunDecl) (r : Lean.Compiler.LCNF.Renaming) :
        Lean.Compiler.LCNF.CompilerM Lean.Compiler.LCNF.FunDecl
        source
        partial def Lean.Compiler.LCNF.Code.applyRenaming (code : Lean.Compiler.LCNF.Code) (r : Lean.Compiler.LCNF.Renaming) :
        Lean.Compiler.LCNF.CompilerM Lean.Compiler.LCNF.Code
        source
        def Lean.Compiler.LCNF.Decl.applyRenaming (decl : Lean.Compiler.LCNF.Decl) (r : Lean.Compiler.LCNF.Renaming) :
        Lean.Compiler.LCNF.CompilerM Lean.Compiler.LCNF.Decl
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For