case class Sub(name: LocalName, target: Term) extends Obj with Product with Serializable
- Alphabetic
- By Inheritance
- Sub
- Serializable
- Serializable
- Product
- Equals
- Obj
- HashEquality
- ShortURIPrinter
- BaseType
- Content
- ClientProperties
- HasMetaData
- AnyRef
- Any
- Hide All
- Show All
- Public
- All
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
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
-
final
def
eq(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef
-
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: None.type
-
final
def
isInstanceOf[T0]: Boolean
- Definition Classes
- Any
- def map(f: (Term) ⇒ Term): Sub
-
def
mdNode: Seq[Node] with AbstractSeq[Node] with Serializable
- Attributes
- protected
- Definition Classes
- Obj
-
val
metadata: MetaData
- Definition Classes
- HasMetaData
- val name: LocalName
-
final
def
ne(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef
-
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): Sub
generic version of substitution that does one step and recurses according to a SubstitutionApplier
-
final
def
synchronized[T0](arg0: ⇒ T0): T0
- Definition Classes
- AnyRef
- val target: Term
-
def
toCML: Node
- Definition Classes
- Obj
- def toCMLQVars(implicit qvars: Context): Node
-
def
toNode: Node
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
toStr(implicit shortURIs: Boolean): String
configurable string representation
configurable string representation
- shortURIs
print OMS without namespace, theory
- Definition Classes
- Sub → ShortURIPrinter
-
def
toString(): String
defaults to toStr(false)
defaults to toStr(false)
- Definition Classes
- ShortURIPrinter → AnyRef → Any
-
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()