Value Members

1.  final def !=(arg0: Any): Boolean

   Definition Classes

   AnyRef → Any

2.  def !==(that: Expr): Formula

   Definition Classes

   Expr

3.  final def ##(): Int

   Definition Classes

   AnyRef → Any

4.  def &(that: Expr): Formula

   Definition Classes

   Expr

5.  def +(other: String): String

   Implicit

   This member is added by an implicit conversion from FOLAtomConst to any2stringadd[FOLAtomConst] performed by method any2stringadd in scala.Predef.

   Definition Classes

   any2stringadd

6.  def -->(that: Expr): Formula

   Definition Classes

   Expr

7.  def ->[B](y: B): (FOLAtomConst, B)

   Implicit

   This member is added by an implicit conversion from FOLAtomConst to ArrowAssoc[FOLAtomConst] performed by method ArrowAssoc in scala.Predef.

   Definition Classes

   ArrowAssoc

   Annotations

   @inline()

8.  def <->(that: Expr): Formula

   Definition Classes

   Expr

9.  final def ==(arg0: Any): Boolean

   Definition Classes

   AnyRef → Any

10.  def ===(that: Expr): Atom

    Definition Classes

    Expr

11.  def ^(n: Int)(that: Expr): Expr

    Definition Classes

    Expr

12.  def alphaEquals(that: Expr): Boolean

    Alpha-equality.

    Alpha-equality.

    that

    Lambda expression to compare against.

    returns

    whether this lambda expression is equal to that lambda expression modulo alpha-conversion.

    Definition Classes

    Expr

13.  def alphaEquivalentHashCode: Int

    Definition Classes

    Const → Expr

14.  def apply(that: FOLTerm*)(implicit dummyImplicit: DummyImplicit): FOLAtom
15.  def apply(that: Expr*)(implicit dummyImplicit: DummyImplicit): Atom

    Definition Classes

    HOLPartialAtom

16.  def apply(that: Iterable[Expr]): Expr

    Definition Classes

    Expr

17.  def apply(that: Expr*): Expr

    Definition Classes

    Expr

18.  def apply(pos: HOLPosition): Expr

    Retrieves this expression's subexpression at a given position.

    Retrieves this expression's subexpression at a given position.

    pos

    The position to be retrieved.

    returns

    The subexpression at pos.

    Definition Classes

    Expr

19.  def apply(p: LambdaPosition): Expr

    Definition Classes

    Expr

20.  final def asInstanceOf[T0]: T0

    Definition Classes

    Any

21.  def clone(): AnyRef

    Attributes

    protected[java.lang]

    Definition Classes

    AnyRef

    Annotations

    @native() @throws( ... )

22.  def contains(exp: Expr): Boolean

    Tests whether an expression is a subexpression.

    Tests whether an expression is a subexpression.

    exp

    The subexpression to be found.

    returns

    A boolean that is true if exp is a subexpression

    Definition Classes

    Expr

23.  def ensuring(cond: (FOLAtomConst) ⇒ Boolean, msg: ⇒ Any): FOLAtomConst

    Implicit

    This member is added by an implicit conversion from FOLAtomConst to Ensuring[FOLAtomConst] performed by method Ensuring in scala.Predef.

    Definition Classes

    Ensuring

24.  def ensuring(cond: (FOLAtomConst) ⇒ Boolean): FOLAtomConst

    Implicit

    This member is added by an implicit conversion from FOLAtomConst to Ensuring[FOLAtomConst] performed by method Ensuring in scala.Predef.

    Definition Classes

    Ensuring

25.  def ensuring(cond: Boolean, msg: ⇒ Any): FOLAtomConst

    Implicit

    This member is added by an implicit conversion from FOLAtomConst to Ensuring[FOLAtomConst] performed by method Ensuring in scala.Predef.

    Definition Classes

    Ensuring

26.  def ensuring(cond: Boolean): FOLAtomConst

    Implicit

    This member is added by an implicit conversion from FOLAtomConst to Ensuring[FOLAtomConst] performed by method Ensuring in scala.Predef.

    Definition Classes

    Ensuring

27.  final def eq(arg0: AnyRef): Boolean

    Definition Classes

    AnyRef

28.  def equals(a: Any): Boolean

    Definition Classes

    Expr → AnyRef → Any

29.  def finalize(): Unit

    Attributes

    protected[java.lang]

    Definition Classes

    AnyRef

    Annotations

    @throws( classOf[java.lang.Throwable] )

30.  def find(exp: Expr): List[HOLPosition]

    Finds all HOL positions of a subexpression in this expression.

    Finds all HOL positions of a subexpression in this expression.

    exp

    The subexpression to be found.

    returns

    A list containing all positions where exp occurs.

    Definition Classes

    Expr

31.  def formatted(fmtstr: String): String

    Implicit

    This member is added by an implicit conversion from FOLAtomConst to StringFormat[FOLAtomConst] performed by method StringFormat in scala.Predef.

    Definition Classes

    StringFormat

    Annotations

    @inline()

32.  def get(pos: HOLPosition): Option[Expr]

    Retrieves this expression's subexpression at a given position, if there is one.

    Retrieves this expression's subexpression at a given position, if there is one.

    pos

    The position to be retrieved.

    returns

    If there is a subexpression at that position, return Some(that expression). Otherwise None.

    Definition Classes

    Expr

33.  def get(p: LambdaPosition): Option[Expr]

    Returns the subexpression at the given position, if it exists.

    Returns the subexpression at the given position, if it exists.

    Definition Classes

    Expr

34.  final def getClass(): Class[_]

    Definition Classes

    AnyRef → Any

    Annotations

    @native()

35.  val hashCode: Int

    Definition Classes

    Const → Expr → AnyRef → Any

36.  def isDefinedAt(pos: HOLPosition): Boolean

    Tests whether this expression has a subexpression at a given position.

    Tests whether this expression has a subexpression at a given position.

    pos

    The position to be tested.

    returns

    Whether this(pos) is defined.

    Definition Classes

    Expr

37.  def isDefinedAt(p: LambdaPosition): Boolean

    Tests whether this Expression has a subexpression at the given position.

    Tests whether this Expression has a subexpression at the given position.

    Definition Classes

    Expr

38.  final def isInstanceOf[T0]: Boolean

    Definition Classes

    Any

39.  val name: String

    Definition Classes

    Const → VarOrConst

40.  final def ne(arg0: AnyRef): Boolean

    Definition Classes

    AnyRef

41.  final def notify(): Unit

    Definition Classes

    AnyRef

    Annotations

    @native()

42.  final def notifyAll(): Unit

    Definition Classes

    AnyRef

    Annotations

    @native()

43.  val params: List[Ty]

    Definition Classes

    Const

44.  def replace(pos: HOLPosition, replacement: Expr): Expr

    Definition Classes

    Expr

45.  def replace(pos: LambdaPosition, replacement: Expr): Expr

    Definition Classes

    Expr

46.  final def synchronized[T0](arg0: ⇒ T0): T0

    Definition Classes

    AnyRef

47.  def syntaxEquals(e: Expr): Boolean

    Syntactic equality (takes names of variables in binders into account).

    Syntactic equality (takes names of variables in binders into account).

    Definition Classes

    Const → Expr

48.  def toAsciiString: String

    Converts this expression into a 7-bit safe ASCII string.

    Converts this expression into a 7-bit safe ASCII string.

    The output can be parsed using e.g. the string interpolators, and we guarantee that the expression can be perfectly reconstructed from the string output.

    Definition Classes

    Expr

49.  def toSigRelativeString(implicit sig: BabelSignature): String

    Converts this expression into a string, taking the signature into account.

    Converts this expression into a string, taking the signature into account.

    This produces a similar output as toString, but will use the variable convention indicated by the signature. That is, if sig defines x to be a constant, then we output just x instead of the default #c(x: i).

    Definition Classes

    Expr

50.  def toString(): String

    Converts this expression into a string.

    Converts this expression into a string.

    The output can be parsed using e.g. the string interpolators, and we guarantee that the expression can be perfectly reconstructed from the string output.

    Definition Classes

    Expr → AnyRef → Any

51.  def toUntypedAsciiString(implicit sig: BabelSignature): String

    Definition Classes

    Expr

52.  def toUntypedString(implicit sig: BabelSignature): String

    Definition Classes

    Expr

53.  val ty: Ty

    Definition Classes

    Const → Expr

54.  def unary_-: Formula

    Definition Classes

    Expr

55.  final def wait(): Unit

    Definition Classes

    AnyRef

    Annotations

    @throws( ... )

56.  final def wait(arg0: Long, arg1: Int): Unit

    Definition Classes

    AnyRef

    Annotations

    @throws( ... )

57.  final def wait(arg0: Long): Unit

    Definition Classes

    AnyRef

    Annotations

    @native() @throws( ... )

58.  def |(that: Expr): Formula

    Definition Classes

    Expr

59.  def →[B](y: B): (FOLAtomConst, B)

    Implicit

    This member is added by an implicit conversion from FOLAtomConst to ArrowAssoc[FOLAtomConst] performed by method ArrowAssoc in scala.Predef.

    Definition Classes

    ArrowAssoc