Documentation

Lean.Compiler.IR.FreeVars

Compute the maximum index M used in a declaration. We M to initialize the fresh index generator used to create fresh variable and join point names.

Recall that we variable and join points share the same namespace in our implementation.

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

      We say a variable (join point) index (aka name) is free in a function body if there isn't a FnBody.vdecl (Fnbody.jdecl) binding it.

      In principle, we can check whether a function body b contains an index i using b.freeIndices.contains i, but it is more efficient to avoid the construction of the set of freeIndices and just search whether i occurs in b or not.

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