# Documentation

Lean.Compiler.IR.ResetReuse

Remark: the insertResetReuse transformation is applied before we have inserted inc/dec instructions, and perfomed lower level optimizations that introduce the instructions release and set.

Remark: the functions S, D and R defined here implement the corresponding functions in the paper "Counting Immutable Beans"

Here are the main differences:

• We use the State monad to manage the generation of fresh variable names.
• Support for join points, and uset and sset instructions for unboxed data.
• D uses the auxiliary function Dmain.
• Dmain returns a pair (b, found) to avoid quadratic behavior when checking the last occurrence of the variable x.
• Because we have join points in the actual implementation, a variable may be live even if it does not occur in a function body. See example at livevars.lean.
@[inline]

We use Context to track join points in scope.

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