Reducibility hints are used in the convertibility checker. When trying to solve a constraint such a
(f ...) =?= (g ...)
g are definitions, the checker has to decide which one will be unfolded.
g) is opaque, then
f) is unfolded if it is also not marked as opaque,
- Else if
g) is abbrev, then
g) is unfolded if
f) is also not marked as abbrev,
- Else if
gare regular, then we unfold the one with the biggest definitional height.
- Otherwise both are unfolded.
The arguments of the
regular constructor are: the definitional height and the flag
The definitional height is by default computed by the kernel. It only takes into account other regular definitions used in a definition. When creating declarations using meta-programming, we can specify the definitional depth manually.
For definitions marked as regular, we also have a hint for constraints such as
(f a) =?= (f b)
self_opt = tt, then checker will first try to solve
a =?= b, only if it fails,
Remark: the hint only affects performance. None of the hints prevent the kernel from unfolding a declaration during type checking.
Remark: the reducibility_hints are not related to the attributes: reducible/irrelevance/semireducible. These attributes are used by the elaborator. The reducibility_hints are used by the kernel (and elaborator). Moreover, the reducibility_hints cannot be changed after a declaration is added to the kernel.