c

info.kwarc.mmt.moduleexpressions

ElaboratedConstant

class ElaboratedConstant extends LazyConstant

Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. ElaboratedConstant
  2. LazyConstant
  3. Constant
  4. HasNotation
  5. HasDefiniens
  6. HasType
  7. Declaration
  8. ContentElement
  9. StructuralElement
  10. NamedElement
  11. Content
  12. ClientProperties
  13. HasMetaData
  14. AnyRef
  15. Any
  1. Hide All
  2. Show All
Visibility
  1. Public
  2. All

Instance Constructors

  1. new ElaboratedConstant(instance: Constant, vd: VarDecl, subss: List[Substitution])

    instance

    the elaborated instance

    vd

    the variable declaration giving rise to this Constant

    subss

    the substitutions that have to be applied to the type/definiens of vd These are applied lazily, i.e., when they are first accessed.

Type Members

  1. type ThisType = Constant

    to allow for sharper types of fields, every subclass of Declaration defines this to be itself

    to allow for sharper types of fields, every subclass of Declaration defines this to be itself

    Definition Classes
    Constant → Declaration

Value Members

  1. final def !=(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  2. final def ##(): Int
    Definition Classes
    AnyRef → Any
  3. final def ==(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  4. var _alias: List[LocalName]
    Attributes
    protected
    Definition Classes
    LazyConstant
  5. var _df: Option[Term]
    Attributes
    protected
    Definition Classes
    LazyConstant
  6. var _not: Option[TextNotation]
    Attributes
    protected
    Definition Classes
    LazyConstant
  7. var _rl: Option[String]
    Attributes
    protected
    Definition Classes
    LazyConstant
  8. var _tp: Option[Term]
    Attributes
    protected
    Definition Classes
    LazyConstant
  9. var _vs: Option[Visibility]
    Attributes
    protected
    Definition Classes
    LazyConstant
  10. def alias: List[LocalName]
    Definition Classes
    LazyConstant → Constant
  11. def alternativeNames: List[LocalName]

    an alternative name

    an alternative name

    None by default; overridden in particular by Constant

    Definition Classes
    Constant → Declaration
  12. final def asInstanceOf[T0]: T0
    Definition Classes
    Any
  13. lazy val clientProperty: ListMap[URI, Any]
    Definition Classes
    ClientProperties
  14. def clone(): AnyRef
    Attributes
    protected[lang]
    Definition Classes
    AnyRef
    Annotations
    @throws( ... ) @native()
  15. def compatible(that: StructuralElement): Boolean

    two StructuralElement's are compatible if they have the same type, same Path, and agree in all parts that are TermContainer's

    two StructuralElement's are compatible if they have the same type, same Path, and agree in all parts that are TermContainer's

    Definition Classes
    StructuralElement
  16. def df: Option[Term]
    Definition Classes
    HasDefiniens
  17. def dfC: TermContainer
    Definition Classes
    LazyConstant → Constant → HasDefiniens
  18. var dfDefined: Boolean
    Attributes
    protected
    Definition Classes
    LazyConstant
  19. def dfNode: Seq[Node] with AbstractSeq[Node] with Serializable
    Definition Classes
    HasDefiniens
  20. def documentHome: DPath
    Definition Classes
    Declaration
  21. final def eq(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  22. def equals(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  23. def equivalentTo(that: StructuralElement): Boolean

    logically equivalent: compares headerInfo, components, and declarations

    logically equivalent: compares headerInfo, components, and declarations

    Definition Classes
    StructuralElement
  24. val feature: String

    the kind of declaration, e.g., "constant"

    the kind of declaration, e.g., "constant"

    Definition Classes
    Constant → ContentElement → StructuralElement
  25. def finalize(): Unit
    Attributes
    protected[lang]
    Definition Classes
    AnyRef
    Annotations
    @throws( classOf[java.lang.Throwable] )
  26. def foreachComponent(f: (CPath, ComponentContainer) ⇒ Unit): Unit

    recursively applies a function to all components in this element (in declaration order)

    recursively applies a function to all components in this element (in declaration order)

    Definition Classes
    ContentElement
  27. def foreachDeclaration(f: (ContentElement) ⇒ Unit): Unit

    recursively applies a function to all declarations in this element (in declaration order)

    recursively applies a function to all declarations in this element (in declaration order)

    Definition Classes
    ContentElement
  28. final def getClass(): Class[_]
    Definition Classes
    AnyRef → Any
    Annotations
    @native()
  29. def getComponent(k: ComponentKey): Option[ComponentContainer]

    returns a specific component if present

    returns a specific component if present

    Definition Classes
    StructuralElement
  30. def getComponentContext(k: ComponentKey): Context

    like getComponent but returns the additional context (in addition to the context of the element) of the component, empty by default, override as needed unspecified if the component does not exist

    like getComponent but returns the additional context (in addition to the context of the element) of the component, empty by default, override as needed unspecified if the component does not exist

    Definition Classes
    StructuralElement
  31. def getComponents: List[DeclarationComponent]

    returns all term components of this elements

    returns all term components of this elements

    Definition Classes
    Constant → StructuralElement
  32. def getDeclarations: Nil.type

    returns all children of this elements

    returns all children of this elements

    Definition Classes
    Constant → Declaration → ContentElement → StructuralElement
  33. def getMetaDataNode: NodeSeq
    Definition Classes
    HasMetaData
  34. def getOrigin: Origin
    Definition Classes
    StructuralElement
  35. def hashCode(): Int
    Definition Classes
    AnyRef → Any
    Annotations
    @native()
  36. def headerInfo: HeaderInfo

    header information of this elements includes the MMT types (e.g., domain, codomain of links) but not the logical types of constants

    header information of this elements includes the MMT types (e.g., domain, codomain of links) but not the logical types of constants

    Definition Classes
    StructuralElement
  37. val home: Term

    the containing module

    the containing module

    this is almost always OMMOD(p:MPath), the main exception are generated anonymous modules

    Definition Classes
    LazyConstant → Declaration
  38. def isGenerated: Boolean
    Definition Classes
    StructuralElement
  39. final def isInstanceOf[T0]: Boolean
    Definition Classes
    Any
  40. def merge(that: Declaration): Constant

    a new declaration with the same path obtained by replacing fields in 'this' with corresponding fields of 'that' Unfortunately, this must take any declaration and throw an error if 'not (that : ThisType)'

    a new declaration with the same path obtained by replacing fields in 'this' with corresponding fields of 'that' Unfortunately, this must take any declaration and throw an error if 'not (that : ThisType)'

    Definition Classes
    Constant → Declaration
  41. def merge(that: StructuralElement): Unit

    merge all properties of 'that' into 'this' except for components and declarations

    merge all properties of 'that' into 'this' except for components and declarations

    Definition Classes
    Declaration → StructuralElement
  42. def mergeError(that: Declaration): Nothing

    called to throw an error from within 'merge'

    called to throw an error from within 'merge'

    Attributes
    protected
    Definition Classes
    Declaration
  43. val metadata: MetaData
    Definition Classes
    HasMetaData
  44. val name: LocalName

    the local name in the containing module

    the local name in the containing module

    for symbols: the name of the symbols

    for assignments: the name of the symbols to which a value is assigned

    Definition Classes
    LazyConstant → Declaration → ContentElement → NamedElement
  45. final def ne(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  46. def not: Option[TextNotation]
    Definition Classes
    HasNotation
  47. def notC: NotationContainer
    Definition Classes
    LazyConstant → HasNotation
  48. def notNode: Seq[Node] with AbstractSeq[Node] with Serializable
    Definition Classes
    HasNotation
  49. final def notify(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native()
  50. final def notifyAll(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native()
  51. def onAccessDf: Unit

    called the first time the definiens is accessed, must set _df

    called the first time the definiens is accessed, must set _df

    Definition Classes
    ElaboratedConstant → LazyConstant
  52. def onAccessOther: Unit

    called the first time anything else is accessed, must set _alias, _rl, and _not

    called the first time anything else is accessed, must set _alias, _rl, and _not

    Definition Classes
    ElaboratedConstant → LazyConstant
  53. def onAccessTp: Unit

    called the first time the type is accessed, must set _tp

    called the first time the type is accessed, must set _tp

    Definition Classes
    ElaboratedConstant → LazyConstant
  54. var otherDefined: Boolean
    Attributes
    protected
    Definition Classes
    LazyConstant
  55. lazy val parent: MPath

    the containing module

    the containing module

    Definition Classes
    Declaration → StructuralElement
  56. def path: GlobalName

    the full MMT URI, parent ? name

    the full MMT URI, parent ? name

    Definition Classes
    Declaration → ContentElement → StructuralElement
  57. def primaryNameAndAliases: (LocalName, List[LocalName])

    returns

    the shortest name and all other names

    Definition Classes
    Declaration
  58. def relativeDocumentHome: LocalName
    Definition Classes
    Declaration
  59. def rl: Option[String]
    Definition Classes
    LazyConstant → Constant
  60. def setDocumentHome(ln: LocalName): Unit
    Definition Classes
    Declaration
  61. def setOrigin(o: Origin): Unit
    Definition Classes
    StructuralElement
  62. final def synchronized[T0](arg0: ⇒ T0): T0
    Definition Classes
    AnyRef
  63. def toNode: Elem

    XML representation

    XML representation

    Definition Classes
    Constant → Content
  64. def toNode(rh: RenderingHandler): Unit

    by default, this prints out toNode

    by default, this prints out toNode

    potentially large StructuralElements should override it with a memory-efficient implementation

    Definition Classes
    Content
  65. def toString(): String
    Definition Classes
    Constant → AnyRef → Any
  66. def toTerm: OMID

    the OMS referencing this declaration

    the OMS referencing this declaration

    Definition Classes
    Declaration → ContentElement
  67. def tp: Option[Term]
    Definition Classes
    HasType
  68. def tpC: TermContainer
    Definition Classes
    LazyConstant → Constant → HasType
  69. var tpDefined: Boolean
    Attributes
    protected
    Definition Classes
    LazyConstant
  70. def tpNode: Seq[Node] with AbstractSeq[Node] with Serializable
    Definition Classes
    HasType
  71. def translate(newHome: Term, prefix: LocalName, translator: Translator, context: Context): FinalConstant

    a recursively translated copy of this declaration with a URI

    a recursively translated copy of this declaration with a URI

    newHome

    the home theory of the result

    prefix

    the prefix used to form the name of the new declaration

    Definition Classes
    Constant → Declaration
  72. def translate(translator: Translator, context: Context): ThisType

    a recursively translated copy of this declaration

    a recursively translated copy of this declaration

    Definition Classes
    Declaration
  73. def translateDf(translator: Translator, context: Context): TermContainer
    Definition Classes
    HasDefiniens
  74. def translateTp(translator: Translator, context: Context): TermContainer
    Definition Classes
    HasType
  75. def vs: Visibility
    Definition Classes
    LazyConstant → Constant
  76. final def wait(): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  77. final def wait(arg0: Long, arg1: Int): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  78. final def wait(arg0: Long): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... ) @native()

Inherited from LazyConstant

Inherited from Constant

Inherited from HasNotation

Inherited from HasDefiniens

Inherited from HasType

Inherited from Declaration

Inherited from ContentElement

Inherited from StructuralElement

Inherited from NamedElement

Inherited from Content

Inherited from ClientProperties

Inherited from HasMetaData

Inherited from AnyRef

Inherited from Any

Ungrouped