object Mizar
- Source
- Utils.scala
Linear Supertypes
Ordering
- Alphabetic
- By Inheritance
Inherited
- Mizar
- AnyRef
- Any
- Hide All
- Show All
Visibility
- Public
- All
Type Members
- class Quantifier extends AnyRef
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
- val HiddenTh: MPath
- val MizarInformal: MPath
- val MizarPatternsTh: MPath
- val MizarTh: MPath
- def adjective(cluster: Term, typ: Term): Term
- def and(tms: List[Term]): Term
- def andCon: GlobalName
- val any: Term
- def apply(f: Term, args: Term*): Term
-
final
def
asInstanceOf[T0]: T0
- Definition Classes
- Any
- def attr(t: Term): Term
- def be(t1: Term, t2: Term): Term
- def by: Term
- def choice(tp: Term): Term
-
def
clone(): AnyRef
- Attributes
- protected[lang]
- Definition Classes
- AnyRef
- Annotations
- @throws( ... ) @native()
- def cluster(a1: Term, a2: Term): Term
- def compact(t: Term): Term
- def constant(name: String): Term
- def constantName(name: String): GlobalName
-
final
def
eq(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef
- def eqCon: GlobalName
-
def
equals(arg0: Any): Boolean
- Definition Classes
- AnyRef → Any
- def falseCon: Term
-
def
finalize(): Unit
- Attributes
- protected[lang]
- Definition Classes
- AnyRef
- Annotations
- @throws( classOf[java.lang.Throwable] )
- def fraenkel(v: String, t: Term, p: Term, f: Term): Term
- def from: Term
-
final
def
getClass(): Class[_]
- Definition Classes
- AnyRef → Any
- Annotations
- @native()
-
def
hashCode(): Int
- Definition Classes
- AnyRef → Any
- Annotations
- @native()
- def is(t1: Term, t2: Term): Term
-
final
def
isInstanceOf[T0]: Boolean
- Definition Classes
- Any
- val mathHubBase: String
- val mmlBase: URI
-
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 num(i: Int): OMLIT
- val numRT: RepresentedRealizedType[BigInt]
- def or(tms: List[Term]): Term
- def orCon: GlobalName
- def prop: Term
- def seqConn(connective: String, length: Term, seq: Term): Term
- def set: Term
-
final
def
synchronized[T0](arg0: ⇒ T0): T0
- Definition Classes
- AnyRef
-
def
toString(): String
- Definition Classes
- AnyRef → Any
- def tp: Term
- def trueCon: Term
-
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()
- object eq extends BinaryLFConstantScala
- object exists extends Quantifier
- object forall extends Quantifier
- object iff extends BinaryLFConstantScala
- object implies extends BinaryLFConstantScala
- object not extends UnaryLFConstantScala
- object proof extends UnaryLFConstantScala