@[reducible, inline]

abbrev Lean.Compiler.LCNF.Renaming : Type

A mapping from free variable id to binder name.

Equations

• Lean.Compiler.LCNF.Renaming = Lean.FVarIdMap Lean.Name

def Lean.Compiler.LCNF.Param.applyRenaming {pu : Purity} (param : Param pu) (r : Renaming) : CompilerM (Param pu)

Equations

• One or more equations did not get rendered due to their size.

def Lean.Compiler.LCNF.LetDecl.applyRenaming {pu : Purity} (decl : LetDecl pu) (r : Renaming) : CompilerM (LetDecl pu)

Equations

• One or more equations did not get rendered due to their size.

partial def Lean.Compiler.LCNF.FunDecl.applyRenaming {pu : Purity} (decl : FunDecl pu) (r : Renaming) : CompilerM (FunDecl pu)

partial def Lean.Compiler.LCNF.Code.applyRenaming {pu : Purity} (code : Code pu) (r : Renaming) : CompilerM (Code pu)

def Lean.Compiler.LCNF.Decl.applyRenaming {pu : Purity} (decl : Decl pu) (r : Renaming) : CompilerM (Decl pu)

Equations

• One or more equations did not get rendered due to their size.