mathlib documentation

core / init.meta.declaration

inductive reducibility_hints  :
Type

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.

Instances for reducibility_hints
meta inductive declaration  :
Type

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

Instances for declaration
meta def mk_definition (n : name) (ls : list name) (v e : expr) :

Instantiate a universe polymorphic declaration type with the given universes.

Instantiate a universe polymorphic declaration value with the given universes.