Documentation

Lean.Compiler.LCNF.Renaming

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

A mapping from free variable id to binder name.

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