Packages

case class Substitution(subs: Sub*) extends Obj with Product with Serializable

substitution between two contexts

Source
Context.scala
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. Substitution
  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 Substitution(subs: Sub*)

Type Members

  1. type ThisType = Substitution

    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
    SubstitutionObj

Value Members

  1. final def !=(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  2. final def ##(): Int
    Definition Classes
    AnyRef → Any
  3. def ++(that: Substitution): Substitution
  4. def ++(s: Sub): Substitution
  5. def ++(n: String, t: Term): Substitution
  6. final def ==(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  7. 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
  8. 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
  9. 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
  10. def apply(v: LocalName): Option[Term]
  11. def asContext: Context

    turns a substitution into a context by treating every substitute as a definiens this permits seeing substitution application as a let-binding

  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 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
  16. def domain: List[LocalName]
  17. final def eq(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  18. def finalize(): Unit
    Attributes
    protected[lang]
    Definition Classes
    AnyRef
    Annotations
    @throws( classOf[java.lang.Throwable] )
  19. 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
  20. final def getClass(): Class[_]
    Definition Classes
    AnyRef → Any
    Annotations
    @native()
  21. def getMetaDataNode: NodeSeq
    Definition Classes
    HasMetaData
  22. 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
  23. lazy val hash: Int

    the hash code

    the hash code

    Definition Classes
    HashEquality
  24. 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
  25. 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
  26. def head: None.type
    Definition Classes
    SubstitutionObj
  27. def isEmpty: Boolean
  28. def isIdentity: Boolean
  29. final def isInstanceOf[T0]: Boolean
    Definition Classes
    Any
  30. def mapTerms(f: (Term) ⇒ Term): Substitution
  31. def maps(n: LocalName): Boolean
  32. def mdNode: Seq[Node] with AbstractSeq[Node] with Serializable
    Attributes
    protected
    Definition Classes
    Obj
  33. val metadata: MetaData
    Definition Classes
    HasMetaData
  34. final def ne(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  35. final def notify(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native()
  36. final def notifyAll(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native()
  37. 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
  38. 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
    SubstitutionObj
  39. 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
  40. val subs: Sub*
  41. def substitute(sub: Substitution)(implicit sa: SubstitutionApplier): Substitution

    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
    SubstitutionObj
  42. final def synchronized[T0](arg0: ⇒ T0): T0
    Definition Classes
    AnyRef
  43. def toCML: Node
    Definition Classes
    Obj
  44. def toCMLQVars(implicit qvars: Context): Elem
    Definition Classes
    SubstitutionObj
  45. def toNode: Elem

    prints to OpenMath

    prints to OpenMath

    Definition Classes
    SubstitutionObjContent
  46. 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
  47. def toOBJNode: Elem

    prints to OpenMath (with OMOBJ wrapper)

    prints to OpenMath (with OMOBJ wrapper)

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

    configurable string representation

    configurable string representation

    shortURIs

    print OMS without namespace, theory

    Definition Classes
    SubstitutionShortURIPrinter
  49. def toString(): String

    defaults to toStr(false)

    defaults to toStr(false)

    Definition Classes
    ShortURIPrinter → AnyRef → Any
  50. final def wait(): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  51. final def wait(arg0: Long, arg1: Int): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  52. 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