case class VarDecl(name: LocalName, feature: Option[String], tp: Option[Term], df: Option[Term], not: Option[TextNotation]) extends Obj with NamedElement with Product with Serializable
represents an MMT term variable declaration
- name
name
- tp
optional type
- df
optional definiens
- not
optional notation
- Source
- Context.scala
- Alphabetic
- By Inheritance
- VarDecl
- Serializable
- Serializable
- Product
- Equals
- NamedElement
- Obj
- HashEquality
- ShortURIPrinter
- BaseType
- Content
- ClientProperties
- HasMetaData
- AnyRef
- Any
- Hide All
- Show All
- Public
- All
Instance Constructors
Type Members
Value Members
-
final
def
!=(arg0: Any): Boolean
- Definition Classes
- AnyRef → Any
-
final
def
##(): Int
- Definition Classes
- AnyRef → Any
-
final
def
==(arg0: Any): Boolean
- Definition Classes
- AnyRef → Any
-
def
^(sub: Substitution): ThisType
applies a substitution to an object (computed immediately) implemented in terms of ^^ and PlainSubstitutionApplier
applies a substitution to an object (computed immediately) implemented in terms of ^^ and PlainSubstitutionApplier
- Definition Classes
- Obj
-
def
^?(sub: Substitution): ThisType
optimized version of substitution defined in terms of SmartSubstitutionApplier
optimized version of substitution defined in terms of SmartSubstitutionApplier
- Definition Classes
- Obj
-
def
^^(sub: Substitution)(implicit sa: SubstitutionApplier): ThisType
convenience method that applies substitution by relegating to a SubstitutionApplier
convenience method that applies substitution by relegating to a SubstitutionApplier
This has the effect that o ^^ sub becomes an infix notation for substitution if an implicit SubstitutionApplier is available.
- Definition Classes
- Obj
-
final
def
asInstanceOf[T0]: T0
- Definition Classes
- Any
-
lazy val
clientProperty: ListMap[URI, Any]
- Definition Classes
- ClientProperties
-
def
clone(): AnyRef
- Attributes
- protected[lang]
- Definition Classes
- AnyRef
- Annotations
- @throws( ... ) @native()
-
def
copy(name: LocalName = this.name, feature: Option[String] = this.feature, tp: Option[Term] = this.tp, df: Option[Term] = this.df, not: Option[TextNotation] = this.not): VarDecl
self-written copy method to copy metadata
-
def
copyFrom(o: Obj): Unit
replaces metadata of this with pointer to those of o
replaces metadata of this with pointer to those of o
- o
the original object call o2.copyFrom(o1) after transforming o1 into o2 in order to preserve metadata
- Definition Classes
- Obj
- val df: Option[Term]
-
final
def
eq(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef
- val feature: Option[String]
-
def
finalize(): Unit
- Attributes
- protected[lang]
- Definition Classes
- AnyRef
- Annotations
- @throws( classOf[java.lang.Throwable] )
-
lazy val
freeVars: List[LocalName]
the free variables of this object in any order
the free variables of this object in any order
- Definition Classes
- Obj
-
final
def
getClass(): Class[_]
- Definition Classes
- AnyRef → Any
- Annotations
- @native()
-
def
getMetaDataNode: NodeSeq
- Definition Classes
- HasMetaData
-
def
governingPath: Option[ContentPath]
the governing path required by Content is the head, if any
the governing path required by Content is the head, if any
- Definition Classes
- Obj
-
lazy val
hash: Int
the hash code
the hash code
- Definition Classes
- HashEquality
-
def
hasheq(that: HashEquality[Obj]): Boolean
this hasheq that is the same as this == that, but fails immediately if false
this hasheq that is the same as this == that, but fails immediately if false
- Definition Classes
- HashEquality
-
def
hashneq(that: HashEquality[Obj]): Boolean
this hasheq that is the same as this == that, but fails immediately if false
this hasheq that is the same as this == that, but fails immediately if false
- Definition Classes
- HashEquality
- def head: Option[ContentPath]
-
final
def
isInstanceOf[T0]: Boolean
- Definition Classes
- Any
-
def
map(f: (Term) ⇒ Term): VarDecl
applies a function to type and definition
-
def
mdNode: Seq[Node] with AbstractSeq[Node] with Serializable
- Attributes
- protected
- Definition Classes
- Obj
-
val
metadata: MetaData
- Definition Classes
- HasMetaData
-
val
name: LocalName
the name relative to the parent
the name relative to the parent
- Definition Classes
- VarDecl → NamedElement
-
final
def
ne(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef
- val not: Option[TextNotation]
-
final
def
notify(): Unit
- Definition Classes
- AnyRef
- Annotations
- @native()
-
final
def
notifyAll(): Unit
- Definition Classes
- AnyRef
- Annotations
- @native()
-
def
subobject(pos: Position): (Context, Obj)
returns the subobject at a given position and its context
returns the subobject at a given position and its context
- Definition Classes
- Obj
-
def
subobjects: List[(Context, Obj)]
all direct subobjects of this object with their context (excluding any outer context of this object)
-
def
subobjectsNoContext(os: List[Obj]): List[(Context, Obj)]
auxiliary function for subobjects in the absence of binding
auxiliary function for subobjects in the absence of binding
- Attributes
- protected
- Definition Classes
- Obj
-
def
substitute(sub: Substitution)(implicit sa: SubstitutionApplier): VarDecl
generic version of substitution that does one step and recurses according to a SubstitutionApplier
-
def
subsumes(that: VarDecl): Boolean
true if this is stronger than that
-
final
def
synchronized[T0](arg0: ⇒ T0): T0
- Definition Classes
- AnyRef
-
def
toCML: Node
- Definition Classes
- Obj
- def toCMLQVars(implicit qvars: Context): Elem
- def toConstant(mp: MPath, con: Context): FinalConstant
- def toDeclaration(home: Term): Declaration
-
def
toNode: Elem
prints to OpenMath
-
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
-
def
toOBJNode: Elem
prints to OpenMath (with OMOBJ wrapper)
prints to OpenMath (with OMOBJ wrapper)
- Definition Classes
- Obj
- def toOML: OML
-
def
toOpenMath: Term
converts to an OpenMath-style attributed variable using two special keys
-
def
toStr(implicit shortURIs: Boolean): String
configurable string representation
configurable string representation
- shortURIs
print OMS without namespace, theory
- Definition Classes
- VarDecl → ShortURIPrinter
-
def
toString(): String
defaults to toStr(false)
defaults to toStr(false)
- Definition Classes
- ShortURIPrinter → AnyRef → Any
- def toTerm: OMV
- val tp: Option[Term]
-
final
def
wait(): Unit
- Definition Classes
- AnyRef
- Annotations
- @throws( ... )
-
final
def
wait(arg0: Long, arg1: Int): Unit
- Definition Classes
- AnyRef
- Annotations
- @throws( ... )
-
final
def
wait(arg0: Long): Unit
- Definition Classes
- AnyRef
- Annotations
- @throws( ... ) @native()