TypeName.{u} (α : Type u) : Type
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

Dynamic : Type
Dynamic : Type

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

This is roughly equivalent to (α : Type) × TypeName α × α, but without the universe bump. Use Dynamic.mk to inject a value into Dynamic from another type, and Dynamic.get? to extract a value from Dynamic if it has some expected type.

Dynamic.mk.{u_1} {α : Type u_1} [TypeName α] (obj : α) : Dynamic
Dynamic.mk.{u_1} {α : Type u_1}
  [TypeName α] (obj : α) : Dynamic

Stores the provided value in a Dynamic.

Use Dynamic.get? α to retrieve it.

Dynamic.get?.{u_1} (α : Type u_1) (any : Dynamic) [TypeName α] :
  Option α
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.