- opaque : reducibility_hints
- abbrev : reducibility_hints
- regular : ℕ → bool → reducibility_hints
Reducibility hints are used in the convertibility checker. When trying to solve a constraint such a
(f ...) =?= (g ...)
where f and g are definitions, the checker has to decide which one will be unfolded. If f (g) is opaque, then g (f) is unfolded if it is also not marked as opaque, Else if f (g) is abbrev, then f (g) is unfolded if g (f) is also not marked as abbrev, Else if f and g are 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 self_opt.
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)
if self_opt == true, then checker will first try to solve (a =?= b), only if it fails, it unfolds f.
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.