3.7. Dynamic Typing

🔗type class
TypeName.{u} (α : Type u) : Type

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
🔗def
Dynamic : Type

Type-tagged union that can store any type with a TypeName instance.

This is roughly equivalent to (α : Type) × TypeName α × α but without the universe bump.

🔗
Dynamic.mk.{u_1} {α : Type u_1} [TypeName α]
    (obj : α) : Dynamic
🔗
Dynamic.get?.{u_1} (α : Type u_1)
    (any : Dynamic) [TypeName α] : Option α

Retrieves the value stored in the Dynamic. Returns some a if the value has the right type, and none otherwise.