def POpaque : Type u

An value of unknown type in a specific universe.

Equations

• POpaque = POpaque.nonemptyType✝.type

@[reducible, inline]

abbrev Opaque : Type

An value of unknown type.

Equations

• Opaque = POpaque

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.

Equations

• Opaque.mk a = POpaque.mk a

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.

Equations

• self.cast = unsafeCast self

@[reducible, inline]

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

Like cast, but with an explicit type.

Equations

• POpaque.castTo α self = self.cast