case class OMSemiFormal(tokens: List[SemiFormalObject]) extends Term with SemiFormalObjectList with Product with Serializable
An OMSemiFormal represents a mathematical object that mixes formal and informal components
- Annotations
- @MMT_TODO( message = ... )
- Deprecated
this should be replaced with the urtheory for semiformal objects
- Source
- Obj.scala
- Alphabetic
- By Inheritance
- OMSemiFormal
- Serializable
- Serializable
- Product
- Equals
- SemiFormalObjectList
- Term
- ThisTypeTrait
- Obj
- HashEquality
- ShortURIPrinter
- BaseType
- Content
- ClientProperties
- HasMetaData
- AnyRef
- Any
- Hide All
- Show All
- Public
- All
Instance Constructors
- new OMSemiFormal(tokens: List[SemiFormalObject])
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
-
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): OMSemiFormal.this.type
applies copyFrom and returns this
applies copyFrom and returns this
- returns
this object but with the metadata from o
- Definition Classes
- 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: None.type
- Definition Classes
- OMSemiFormal → Obj
-
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)
all direct subobjects of this object with their context (excluding any outer context of this object)
- Definition Classes
- OMSemiFormal → 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
-
def
substitute(sub: Substitution)(implicit sa: SubstitutionApplier): OMSemiFormal
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
- OMSemiFormal → 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
- OMSemiFormal → Obj
-
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
- Definition Classes
- SemiFormalObjectList
-
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
- OMSemiFormal → ShortURIPrinter
-
def
toString(): String
- Definition Classes
- SemiFormalObjectList → AnyRef → Any
-
val
tokens: List[SemiFormalObject]
- Definition Classes
- OMSemiFormal → SemiFormalObjectList
-
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()