Packages

sealed abstract class Term extends Obj with ThisTypeTrait

Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. Term
  2. ThisTypeTrait
  3. Obj
  4. HashEquality
  5. ShortURIPrinter
  6. BaseType
  7. Content
  8. ClientProperties
  9. HasMetaData
  10. AnyRef
  11. Any
  1. Hide All
  2. Show All
Visibility
  1. Public
  2. All

Type Members

  1. final type ThisType = Term

    the type of this instance

    the type of this instance

    This is needed to provide sharper return types for inductive functions, e.g., substitution returns Term if applied to Term, Context if applied to Context, etc.

    Definition Classes
    Term → Obj

Abstract Value Members

  1. abstract def head: Option[ContentPath]
    Definition Classes
    Obj
  2. abstract def subobjects: List[(Context, Obj)]

    all direct subobjects of this object with their context (excluding any outer context of this object)

    all direct subobjects of this object with their context (excluding any outer context of this object)

    Definition Classes
    Obj
  3. abstract def substitute(sub: Substitution)(implicit sa: SubstitutionApplier): ThisType

    generic version of substitution that does one step and recurses according to a SubstitutionApplier

    generic version of substitution that does one step and recurses according to a SubstitutionApplier

    capture is avoided by renaming bound variables that are free in sub

    Individual SubstitutionAppliers can default to this method in order to recurse one level.

    Definition Classes
    Obj
  4. abstract def toCMLQVars(implicit qvars: Context): Node
    Definition Classes
    Obj
  5. abstract def toNode: Node

    prints to OpenMath

    prints to OpenMath

    Definition Classes
    Obj → Content
  6. abstract def toStr(implicit shortURIs: Boolean): String

    configurable string representation

    configurable string representation

    shortURIs

    print OMS without namespace, theory

    Definition Classes
    ShortURIPrinter

Concrete 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. 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
  5. 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
  6. 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
  7. def apply(args: Term*): OMA

    permits the intuitive f(t_1,...,t_n) syntax for term applications

  8. final def asInstanceOf[T0]: T0
    Definition Classes
    Any
  9. lazy val clientProperty: ListMap[URI, Any]
    Definition Classes
    ClientProperties
  10. def clone(): AnyRef
    Attributes
    protected[lang]
    Definition Classes
    AnyRef
    Annotations
    @throws( ... ) @native()
  11. 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
  12. final def eq(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  13. def equals(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  14. def finalize(): Unit
    Attributes
    protected[lang]
    Definition Classes
    AnyRef
    Annotations
    @throws( classOf[java.lang.Throwable] )
  15. 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
  16. def from(o: Term): Term.this.type

    applies copyFrom and returns this

    applies copyFrom and returns this

    returns

    this object but with the metadata from o

  17. final def getClass(): Class[_]
    Definition Classes
    AnyRef → Any
    Annotations
    @native()
  18. def getMetaDataNode: NodeSeq
    Definition Classes
    HasMetaData
  19. 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
  20. lazy val hash: Int

    the hash code

    the hash code

    Definition Classes
    HashEquality
  21. def hashCode(): Int
    Definition Classes
    AnyRef → Any
    Annotations
    @native()
  22. 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
  23. 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
  24. final def isInstanceOf[T0]: Boolean
    Definition Classes
    Any
  25. def mdNode: Seq[Node] with AbstractSeq[Node] with Serializable
    Attributes
    protected
    Definition Classes
    Obj
  26. val metadata: MetaData
    Definition Classes
    HasMetaData
  27. final def ne(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  28. final def notify(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native()
  29. final def notifyAll(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native()
  30. def strip: Term
  31. 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
  32. 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
  33. final def synchronized[T0](arg0: ⇒ T0): T0
    Definition Classes
    AnyRef
  34. def toCML: Node
    Definition Classes
    Obj
  35. def toMPath: MPath

    the syntactically computed MPath of the term.

    the syntactically computed MPath of the term. If the term is module level, this is guaranteed to be correct.

  36. 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
  37. def toOBJNode: Elem

    prints to OpenMath (with OMOBJ wrapper)

    prints to OpenMath (with OMOBJ wrapper)

    Definition Classes
    Obj
  38. def toString(): String

    defaults to toStr(false)

    defaults to toStr(false)

    Definition Classes
    ShortURIPrinter → AnyRef → Any
  39. final def wait(): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  40. final def wait(arg0: Long, arg1: Int): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  41. final def wait(arg0: Long): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... ) @native()

Inherited from ThisTypeTrait

Inherited from Obj

Inherited from HashEquality[Obj]

Inherited from ShortURIPrinter

Inherited from BaseType

Inherited from Content

Inherited from ClientProperties

Inherited from HasMetaData

Inherited from AnyRef

Inherited from Any

Ungrouped