def POpaque : Type u

An value of unknown type in a specific universe.

@[reducible, inline]

abbrev Opaque : Type

An value of unknown type.

instance POpaque.instNonempty : Nonempty POpaque

opaque POpaque.mk {α : Type u} (a : α) : POpaque

Cast away a value's type and universe.

@[reducible, inline]

abbrev Opaque.mk {α : Type u} (a : α) : Opaque

Cast away a value's type and universe.

unsafe def POpaque.cast {α : Type u} (self : POpaque) : α

Cast an opaque value to a specific type.

This operation is unsafe because there is no guarantee that the opaque value is of type α or it its rea; value can soundly fit inside the opaque value's universe.

@[reducible, inline]

unsafe abbrev POpaque.castTo (α : Type u) (self : POpaque) : α

Like cast, but with an explicit type.