Documentation

Lean.Compiler.IR.NormIds

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

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

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

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

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

Equations