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 #

reflected_univ.{u}: A typeclass for reflecting the universe u to a level.
reflect_univ.{u} : level: Obtain the level of a universe by typeclass search.
tactic.interactive.reflect_name: solve goals of the form reflected (@foo.{u v}) by searching for reflected_univ.{u} instances.

source

@[class]

meta structure reflected_univ :

Type

lvl : level

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

source

meta def reflect_univ [reflected_univ] :

level

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

source

@[protected, instance]

meta def reflect_univ.zero :

reflected_univ

source

@[protected, instance]

meta def reflect_univ.succ [reflected_univ] :

reflected_univ

source

@[protected, instance]

meta def reflect_univ.max [reflected_univ] [reflected_univ] :

reflected_univ

source

@[protected, instance]

meta def reflect_univ.imax [reflected_univ] [reflected_univ] :

reflected_univ

source

meta def tactic.interactive.reflect_name :

tactic unit

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

source

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

reflected (Π (a : α) (b : β a), γ a b) f → reflected α a → reflected (β a) b → reflected (γ a b) (f a b)

Convenience helper for two consecutive reflected.subst applications

source

meta def reflected.subst₃ {α : Sort u} {β : α → Sort v} {γ : Π (a : α), β a → Sort w} {δ : Π (a : α) (b : β a), γ a b → Sort 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) f → reflected α a → reflected (β a) b → reflected (γ a b) c → reflected (δ a b c) (f a b c)

Convenience helper for three consecutive reflected.subst applications

source

meta def reflected.subst₄ {α : Sort u} {β : α → Sort v} {γ : Π (a : α), β a → Sort w} {δ : Π (a : α) (b : β a), γ a b → Sort x} {ε : Π (a : α) (b : β a) (c : γ a b), δ a b c → Sort 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) f → reflected α a → reflected (β a) b → reflected (γ a b) c → reflected (δ a b c) d → reflected (ε a b c d) (f a b c d)

Convenience helper for four consecutive reflected.subst applications