Packages

case class Sub(name: LocalName, target: Term) extends Obj with Product with Serializable

a case in a substitution

Source
Context.scala
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. Sub
  2. Serializable
  3. Serializable
  4. Product
  5. Equals
  6. Obj
  7. HashEquality
  8. ShortURIPrinter
  9. BaseType
  10. Content
  11. ClientProperties
  12. HasMetaData
  13. AnyRef
  14. Any
  1. Hide All
  2. Show All
Visibility
  1. Public
  2. All

Instance Constructors

  1. new Sub(name: LocalName, target: Term)

Type Members

  1. type ThisType = Sub

    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
    SubObj

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. final def asInstanceOf[T0]: T0
    Definition Classes
    Any
  8. lazy val clientProperty: ListMap[URI, Any]
    Definition Classes
    ClientProperties
  9. def clone(): AnyRef
    Attributes
    protected[lang]
    Definition Classes
    AnyRef
    Annotations
    @throws( ... ) @native()
  10. 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
  11. final def eq(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  12. def finalize(): Unit
    Attributes
    protected[lang]
    Definition Classes
    AnyRef
    Annotations
    @throws( classOf[java.lang.Throwable] )
  13. 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
  14. final def getClass(): Class[_]
    Definition Classes
    AnyRef → Any
    Annotations
    @native()
  15. def getMetaDataNode: NodeSeq
    Definition Classes
    HasMetaData
  16. 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
  17. lazy val hash: Int

    the hash code

    the hash code

    Definition Classes
    HashEquality
  18. 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
  19. 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
  20. def head: None.type
    Definition Classes
    SubObj
  21. final def isInstanceOf[T0]: Boolean
    Definition Classes
    Any
  22. def map(f: (Term) ⇒ Term): Sub
  23. def mdNode: Seq[Node] with AbstractSeq[Node] with Serializable
    Attributes
    protected
    Definition Classes
    Obj
  24. val metadata: MetaData
    Definition Classes
    HasMetaData
  25. val name: LocalName
  26. final def ne(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  27. final def notify(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native()
  28. final def notifyAll(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native()
  29. 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
  30. 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
    SubObj
  31. 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
  32. def substitute(sub: Substitution)(implicit sa: SubstitutionApplier): Sub

    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
    SubObj
  33. final def synchronized[T0](arg0: ⇒ T0): T0
    Definition Classes
    AnyRef
  34. val target: Term
  35. def toCML: Node
    Definition Classes
    Obj
  36. def toCMLQVars(implicit qvars: Context): Node
    Definition Classes
    SubObj
  37. def toNode: Node

    prints to OpenMath

    prints to OpenMath

    Definition Classes
    SubObjContent
  38. 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
  39. def toOBJNode: Elem

    prints to OpenMath (with OMOBJ wrapper)

    prints to OpenMath (with OMOBJ wrapper)

    Definition Classes
    Obj
  40. def toStr(implicit shortURIs: Boolean): String

    configurable string representation

    configurable string representation

    shortURIs

    print OMS without namespace, theory

    Definition Classes
    SubShortURIPrinter
  41. def toString(): String

    defaults to toStr(false)

    defaults to toStr(false)

    Definition Classes
    ShortURIPrinter → AnyRef → Any
  42. final def wait(): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  43. final def wait(arg0: Long, arg1: Int): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  44. final def wait(arg0: Long): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... ) @native()

Inherited from Serializable

Inherited from Serializable

Inherited from Product

Inherited from Equals

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