scilib documentation

• 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 = tt, 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.