Documentation

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
Instances
    unsafe def TypeName.mk (α : Type u) (typeName : Lake.Name) :

    Creates a TypeName instance.

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

    Equations
    Instances For
      @[implemented_by _private.Init.Dynamic.0.TypeName.typeNameImpl]
      opaque TypeName.typeName (α : Type u_1) [TypeName α] :

      Returns a declaration name of the 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.

      Equations
      Instances For
        @[implemented_by _private.Init.Dynamic.0.Dynamic.typeNameImpl]

        The name of the type of the value stored in the Dynamic.

        @[implemented_by _private.Init.Dynamic.0.Dynamic.get?Impl]
        opaque Dynamic.get? (α : Type u_1) (any : Dynamic) [TypeName α] :

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

        @[implemented_by _private.Init.Dynamic.0.Dynamic.mkImpl]
        opaque Dynamic.mk {α : Type u_1} [TypeName α] (obj : α) :