Documentation

Lean.Compiler.LCNF.FixedArgs

Given the (potentially mutually) recursive declarations decls, return a map from declaration name decl.name to a bit-mask m where m[i] is true iff the decl.params[i] is a fixed argument. That is, it does not change in recursive applications. The function assumes that if a function f was declared in a mutual block, then decls contains all (computationally relevant) functions in the mutual block.

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