case class Substitution(subs: Sub*) extends Obj with Product with Serializable
- Alphabetic
- By Inheritance
- Substitution
- Serializable
- Serializable
- Product
- Equals
- Obj
- HashEquality
- ShortURIPrinter
- BaseType
- Content
- ClientProperties
- HasMetaData
- AnyRef
- Any
- Hide All
- Show All
- Public
- All
Type Members
-
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
- Substitution → Obj
Value Members
-
final
def
!=(arg0: Any): Boolean
- Definition Classes
- AnyRef → Any
-
final
def
##(): Int
- Definition Classes
- AnyRef → Any
- def ++(that: Substitution): Substitution
- def ++(s: Sub): Substitution
- def ++(n: String, t: Term): Substitution
-
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
- def apply(v: LocalName): Option[Term]
-
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
-
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
- def domain: List[LocalName]
-
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
- Definition Classes
- Substitution → Obj
- def isEmpty: Boolean
- def isIdentity: Boolean
-
final
def
isInstanceOf[T0]: Boolean
- Definition Classes
- Any
- def mapTerms(f: (Term) ⇒ Term): Substitution
- def maps(n: LocalName): Boolean
-
def
mdNode: Seq[Node] with AbstractSeq[Node] with Serializable
- Attributes
- protected
- Definition Classes
- Obj
-
val
metadata: MetaData
- Definition Classes
- HasMetaData
-
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)
all direct subobjects of this object with their context (excluding any outer context of this object)
- Definition Classes
- Substitution → Obj
-
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
- val subs: Sub*
-
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
- Substitution → Obj
-
final
def
synchronized[T0](arg0: ⇒ T0): T0
- Definition Classes
- AnyRef
-
def
toCML: Node
- Definition Classes
- Obj
-
def
toCMLQVars(implicit qvars: Context): Elem
- Definition Classes
- Substitution → Obj
-
def
toNode: Elem
prints to OpenMath
prints to OpenMath
- Definition Classes
- Substitution → Obj → Content
-
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
- Substitution → 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()