mathlib 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 == 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.

• defn : name → list name → expr → expr → reducibility_hints → bool → declaration
• thm : name → list name → expr → task expr → declaration
• cnst : name → list name → expr → bool → declaration
• ax : name → list name → expr → declaration

Reflect a C++ declaration object. The VM replaces it with the C++ implementation.