# Documentation

Lean.Compiler.IR.NormIds

@[inline]
Equations
Equations
Equations
Equations
• One or more equations did not get rendered due to their size.

Return true if variable, parameter and join point ids are unique

Equations
@[inline]
Equations
Equations
• = match with | some y => y | none => x
Equations
• = match x with | => | other => pure other
Equations
Equations
• One or more equations did not get rendered due to their size.
@[inline]
Equations
@[inline]
Equations
@[inline]
Equations
@[inline]
def Lean.IR.NormalizeIds.withParams {α : Type} (ps : ) (k : ) :
Equations
• One or more equations did not get rendered due to their size.
Equations
Equations
• One or more equations did not get rendered due to their size.

Create a declaration equivalent to d s.t. d.normalizeIds.uniqueIds == true

Equations

Apply a function f : VarId → VarId to variable occurrences. The following functions assume the IR code does not have variable shadowing.

@[inline]
Equations
def Lean.IR.MapVars.mapArgs (f : ) (as : ) :
Equations
Equations
• One or more equations did not get rendered due to their size.
partial def Lean.IR.MapVars.mapFnBody (f : ) :
@[inline]
Equations

Replace x with y in b. This function assumes b does not shadow x

Equations