Expand description
Code to check whether refinement parameters are used in allowed positions.
The correct usage of a parameter depends on whether its infer mode is evar or kvar. For evar mode, parameters must be used at least once as an index in a position that fully determines their value (see https://arxiv.org/pdf/2209.13000.pdf for details). Parameters with kvar mode (i.e., abstract refinement predicates) must only be used in function position in a top-level conjunction such that they result in a proper horn constraint after being substituted by a kvar as required by fixpoint.
Structs§
Functions§
- check 🔒
Type Aliases§
- Result 🔒