Init.Dynamic

class TypeName (α : Type u) :

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

mk' :: (

data : (TypeNameData✝ α).type

)

Instances

source

instance instNonemptyTypeName {α : Type u_1} :

Nonempty (TypeName α)

source

unsafe def TypeName.mk (α : Type u) (typeName : Lean.Name) :

TypeName α

Creates a TypeName instance.

For safety, it is required that the constant typeName is definitionally equal to α.

Equations

TypeName.mk α typeName = { data := unsafeCast typeName }

Instances For

source

@[implemented_by _private.Init.Dynamic.0.TypeName.typeNameImpl]

opaque TypeName.typeName (α : Type u_1) [TypeName α] :

Lean.Name

Returns a declaration name of the type.

source

def 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.

Equations