def Lake.POpaque : Type u

An value of unknown type in a specific universe.

Equations

• Lake.POpaque = Lake.POpaque.nonemptyType✝.type

@[reducible, inline]

abbrev Lake.Opaque : Type

An value of unknown type.

Equations

• Lake.Opaque = Lake.POpaque

instance Lake.POpaque.instNonempty : Nonempty POpaque

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

Cast away a value's type and universe.

@[reducible, inline]

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

Cast away a value's type and universe.

Equations

• Opaque.mk a = Lake.POpaque.mk a

unsafe def Lake.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 that its real value can soundly fit inside the opaque value's universe.

Equations

• self.cast = unsafeCast self

@[reducible, inline]

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

Like cast, but with an explicit type.

Equations

• Lake.POpaque.castTo α self = self.cast