# Documentation

Value used in the abstract interpreter

Instances For
Equations

In truncate, we approximate a value as top if depth > truncateMaxDepth. TODO: add option to control this parameter.

Equations

Make sure constructors of recursive inductive datatypes can only occur once in each path. Values at depth > truncateMaxDepth are also approximated at top. We use this function this function to implement a simple widening operation for our abstract interpreter. Recall the widening functions is used to ensure termination in abstract interpreters.

Equations

Widening operator that guarantees termination in our abstract interpreter.

Equations
Equations
Equations
• One or more equations did not get rendered due to their size.
Instances For
• assignments :
Instances For
@[inline]
Equations
Equations
• One or more equations did not get rendered due to their size.
Equations
• = match arg with | => | x => pure Lean.IR.UnreachableBranches.Value.top
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.

Return true if the assignment of at least one parameter has been updated.

Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
def Lean.IR.elimDeadBranches (decls : ) :
Equations
• One or more equations did not get rendered due to their size.