mathlib documentation

meta.univs

Reflection of universe variables #

The reflect and has_reflect machinery (sometimes via the `(expr) syntax) allows terms to be converted to the expression that constructs them. However, this construction does not support universe variables.

This file provides a typeclass reflected_univ.{u} to match a universe variable u with a level l, which allows reflect to be used universe-polymorphically.

Main definitions #

@[class]
meta structure reflected_univ  :
Type

A typeclass to translate a universe argument into a level. Note that level.mvar and level.param are not supported.

Note that the instance_priority linter will complain if instance of this class have the default priority, as it takes no arguments! Since it doesn't make any difference, we do what the linter asks.

Instances of this typeclass

Reflect a universe variable u into a level via typeclass search.

@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]

Reflect a universe-polymorphic name, by searching for reflected_univ instances.

meta def reflected.subst₂ {α : Sort u} {β : α → Sort v} {γ : Π (a : α), β aSort w} {f : Π (a : α) (b : β a), γ a b} {a : α} {b : β a} :
reflected (Π (a : α) (b : β a), γ a b) freflected α areflected (β a) breflected (γ a b) (f a b)

Convenience helper for two consecutive reflected.subst applications

meta def reflected.subst₃ {α : Sort u} {β : α → Sort v} {γ : Π (a : α), β aSort w} {δ : Π (a : α) (b : β a), γ a bSort x} {f : Π (a : α) (b : β a) (c : γ a b), δ a b c} {a : α} {b : β a} {c : γ a b} :
reflected (Π (a : α) (b : β a) (c : γ a b), δ a b c) freflected α areflected (β a) breflected (γ a b) creflected (δ a b c) (f a b c)

Convenience helper for three consecutive reflected.subst applications

meta def reflected.subst₄ {α : Sort u} {β : α → Sort v} {γ : Π (a : α), β aSort w} {δ : Π (a : α) (b : β a), γ a bSort x} {ε : Π (a : α) (b : β a) (c : γ a b), δ a b cSort y} {f : Π (a : α) (b : β a) (c : γ a b) (d : δ a b c), ε a b c d} {a : α} {b : β a} {c : γ a b} {d : δ a b c} :
reflected (Π (a : α) (b : β a) (c : γ a b) (d : δ a b c), ε a b c d) freflected α areflected (β a) breflected (γ a b) creflected (δ a b c) dreflected (ε a b c d) (f a b c d)

Convenience helper for four consecutive reflected.subst applications

Universe-polymorphic has_reflect instances #

@[protected, instance]

Universe polymorphic version of the builtin punit.reflect.

@[protected, instance]
meta def list.reflect' [reflected_univ] {α : Type u} [has_reflect α] [reflected (Type u) α] :

Universe polymorphic version of the builtin list.reflect.

@[protected, instance]
meta def ulift.reflect' [reflected_univ] [reflected_univ] {α : Type v} [reflected (Type v) α] [has_reflect α] :