case class OMA(fun: Term, args: List[Term]) extends Term with Product with Serializable
An OMA represents an application of a term to a list of terms
- fun
the function term
- args
the list of argument terms (may be Nil)
- Source
- Obj.scala
- Alphabetic
- By Inheritance
- OMA
- Serializable
- Serializable
- Product
- Equals
- Term
- ThisTypeTrait
- Obj
- HashEquality
- ShortURIPrinter
- BaseType
- Content
- ClientProperties
- HasMetaData
- AnyRef
- Any
- Hide All
- Show All
- Public
- All
Instance Constructors
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
-
def
apply(args: Term*): OMA
permits the intuitive f(t_1,...,t_n) syntax for term applications
permits the intuitive f(t_1,...,t_n) syntax for term applications
- Definition Classes
- Term
- val args: List[Term]
-
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
-
def
from(o: Term): OMA.this.type
applies copyFrom and returns this
applies copyFrom and returns this
- returns
this object but with the metadata from o
- Definition Classes
- Term
- val fun: Term
-
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: Option[ContentPath]
-
final
def
isInstanceOf[T0]: Boolean
- Definition Classes
- Any
-
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
strip: Term
- Definition Classes
- Term
-
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): OMA
generic version of substitution that does one step and recurses according to a SubstitutionApplier
-
final
def
synchronized[T0](arg0: ⇒ T0): T0
- Definition Classes
- AnyRef
-
def
toCML: Node
- Definition Classes
- Obj
- def toCMLQVars(implicit qvars: Context): Elem
-
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.
- Definition Classes
- Term
-
def
toNode: Elem
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
- OMA → 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()