class TypeName (α : 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

• mk' :: (
• data : (TypeNameData✝ α).type
• )

Instances

• Lean.Elab.Command.instTypeNameMacroExpandedSnapshot
• Lean.Elab.Tactic.GuardMsgs.instTypeNameGuardMsgFailure
• Lean.Elab.Term.instTypeNameBodyInfo
• Lean.Elab.instTypeNameDefsParsedSnapshot
• Lean.Elab.instTypeNameInlayHint
• Lean.Language.instTypeNameSnapshotLeaf
• Lean.Language.instTypeNameSnapshotTree
• Lean.Meta.Tactic.TryThis.instTypeNameTryThisInfo
• Lean.Meta.instTypeNameRealizeConstantResult
• Lean.Server.FileWorker.instTypeNameInlayHintState
• Lean.Server.FileWorker.instTypeNameMemorizedInteractiveDiagnostics
• Lean.Server.FileWorker.instTypeNameSemanticTokensState
• Lean.Widget.instTypeNameContextInfo
• Lean.Widget.instTypeNameInfoWithCtx
• Lean.Widget.instTypeNameLazyTraceChildren
• Lean.Widget.instTypeNameLocalContext
• Lean.Widget.instTypeNameMessageData
• Lean.Widget.instTypeNameTermInfo
• Lean.instTypeNameMessageData

instance instNonemptyTypeName {α : Type u_1} : Nonempty (TypeName α)

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 }

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

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

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

Equations

• Dynamic = DynamicPointed✝.type

Instances For

• instNonemptyDynamic

instance instNonemptyDynamic : Nonempty Dynamic

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

opaque Dynamic.typeName (any : Dynamic) : Lean.Name

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 α] : Option α

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 : α) : Dynamic