Dynamic type name information.
Types with an instance of TypeName
can be stored in an Dynamic
.
The type class contains the declaration name of the type,
which must not have any universe parameters
and be of type Sort ..
(i.e., monomorphic).
The preferred way to declare instances of this type is using the derive
handler, which will internally use the unsafe TypeName.mk
function.
Morally, this is the same as:
class TypeName (α : Type) where unsafe mk :: typeName : Name
Methods
data | : | (TypeNameData✝ α).type |