gapt
2.18.0-SNAPSHOT
API
Generated with
gapt/gapt/gapt.expr/gapt.expr.formula/gapt.expr.formula.fol/FOLFormula

FOLFormula

gapt.expr.formula.fol.FOLFormula
trait FOLFormula extends Formula, FOLExpression

Attributes

Source
FOLFormula.scala
Graph
Supertypes
trait Formula
class Expr
class Object
trait Matchable
class Any
Show all
Known subtypes
trait FOLAtom
trait PropAtom
trait PropFormula

Members list

Value members

Concrete methods

def &(that: FOLFormula): FOLFormula

Attributes

Source
FOLFormula.scala
def -->(that: FOLFormula): FOLFormula

Attributes

Source
FOLFormula.scala
def <->(that: FOLFormula): FOLFormula

Attributes

Source
FOLFormula.scala
override def unary_-: FOLFormula

Attributes

Definition Classes
Source
FOLFormula.scala
def |(that: FOLFormula): FOLFormula

Attributes

Source
FOLFormula.scala

Inherited methods

def !==(that: Expr): Formula

Attributes

Inherited from:
Expr
Source
typedLambdaCalculus.scala
def &(that: Expr): Formula

Attributes

Inherited from:
Expr
Source
typedLambdaCalculus.scala
def -->(that: Expr): Formula

Attributes

Inherited from:
Expr
Source
typedLambdaCalculus.scala
def <->(that: Expr): Formula

Attributes

Inherited from:
Expr
Source
typedLambdaCalculus.scala
def ===(that: Expr): Atom

Attributes

Inherited from:
Expr
Source
typedLambdaCalculus.scala
def ^(n: Int)(that: Expr): Expr

Attributes

Inherited from:
Expr
Source
typedLambdaCalculus.scala
def alphaEquals(that: Expr): Boolean

Alpha-equality.

Alpha-equality.

Value parameters

that

Lambda expression to compare against.

Attributes

Returns

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

Inherited from:
Expr
Source
typedLambdaCalculus.scala
def alphaEquivalentHashCode: Int

Attributes

Inherited from:
Expr
Source
typedLambdaCalculus.scala
def apply(pos: FOLPosition): FOLExpression

Retrieves this expression's subexpression at a given position.

Retrieves this expression's subexpression at a given position.

Value parameters

pos

The position to be retrieved.

Attributes

Returns

The subexpression at pos.

Inherited from:
FOLExpression
Source
FOLExpression.scala
def apply(that: Iterable[Expr]): Expr

Attributes

Inherited from:
Expr
Source
typedLambdaCalculus.scala
def apply(that: Expr*): Expr

Attributes

Inherited from:
Expr
Source
typedLambdaCalculus.scala
def apply(pos: HOLPosition): Expr

Retrieves this expression's subexpression at a given position.

Retrieves this expression's subexpression at a given position.

Value parameters

pos

The position to be retrieved.

Attributes

Returns

The subexpression at pos.

Inherited from:
Expr
Source
typedLambdaCalculus.scala
def apply(p: LambdaPosition): Expr

Attributes

Inherited from:
Expr
Source
typedLambdaCalculus.scala
def contains(exp: Expr): Boolean

Tests whether an expression is a subexpression.

Tests whether an expression is a subexpression.

Value parameters

exp

The subexpression to be found.

Attributes

Returns

A boolean that is true if exp is a subexpression

Inherited from:
Expr
Source
typedLambdaCalculus.scala
override def equals(a: Any): Boolean

Compares the receiver object (this) with the argument object (that) for equivalence.

Compares the receiver object (this) with the argument object (that) for equivalence.

Any implementation of this method should be an equivalence relation:

  • It is reflexive: for any instance x of type Any, x.equals(x) should return true.
  • It is symmetric: for any instances x and y of type Any, x.equals(y) should return true if and only if y.equals(x) returns true.
  • It is transitive: for any instances x, y, and z of type Any if x.equals(y) returns true and y.equals(z) returns true, then x.equals(z) should return true.

If you override this method, you should verify that your implementation remains an equivalence relation. Additionally, when overriding this method it is usually necessary to override hashCode to ensure that objects which are "equal" (o1.equals(o2) returns true) hash to the same scala.Int. (o1.hashCode.equals(o2.hashCode)).

Value parameters

that

the object to compare against this object for equality.

Attributes

Returns

true if the receiver object is equivalent to the argument; false otherwise.

Definition Classes
Expr -> Any
Inherited from:
Expr
Source
typedLambdaCalculus.scala
def find(exp: FOLExpression): List[FOLPosition]

Finds all HOL positions of a subexpression in this expression.

Finds all HOL positions of a subexpression in this expression.

Value parameters

exp

The subexpression to be found.

Attributes

Returns

A list containing all positions where exp occurs.

Inherited from:
FOLExpression
Source
FOLExpression.scala
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.

Value parameters

exp

The subexpression to be found.

Attributes

Returns

A list containing all positions where exp occurs.

Inherited from:
Expr
Source
typedLambdaCalculus.scala
def get(pos: FOLPosition): Option[FOLExpression]

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.

Value parameters

pos

The position to be retrieved.

Attributes

Returns

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

Inherited from:
FOLExpression
Source
FOLExpression.scala
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.

Value parameters

pos

The position to be retrieved.

Attributes

Returns

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

Inherited from:
Expr
Source
typedLambdaCalculus.scala
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.

Attributes

Inherited from:
Expr
Source
typedLambdaCalculus.scala
def hashCode: Int

Calculate a hash code value for the object.

Calculate a hash code value for the object.

The default hashing algorithm is platform dependent.

Note that it is allowed for two objects to have identical hash codes (o1.hashCode.equals(o2.hashCode)) yet not be equal (o1.equals(o2) returns false). A degenerate implementation could always return 0. However, it is required that if two objects are equal (o1.equals(o2) returns true) that they have identical hash codes (o1.hashCode.equals(o2.hashCode)). Therefore, when overriding this method, be sure to verify that the behavior is consistent with the equals method.

Attributes

Returns

the hash code value for this object.

Inherited from:
Expr
Source
typedLambdaCalculus.scala
def isDefinedAt(pos: FOLPosition): Boolean

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

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

Value parameters

pos

The position to be tested.

Attributes

Returns

Whether this(pos) is defined.

Inherited from:
FOLExpression
Source
FOLExpression.scala
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.

Value parameters

pos

The position to be tested.

Attributes

Returns

Whether this(pos) is defined.

Inherited from:
Expr
Source
typedLambdaCalculus.scala
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.

Attributes

Inherited from:
Expr
Source
typedLambdaCalculus.scala
def replace(pos: FOLPosition, replacement: FOLExpression): FOLExpression

Attributes

Inherited from:
FOLExpression
Source
FOLExpression.scala
override def replace(pos: HOLPosition, exp: Expr): Formula

Attributes

Definition Classes
Inherited from:
Formula
Source
Formula.scala
def replace(pos: LambdaPosition, replacement: Expr): Expr

Attributes

Inherited from:
Expr
Source
typedLambdaCalculus.scala
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).

Attributes

Inherited from:
Expr
Source
typedLambdaCalculus.scala
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.

Attributes

Inherited from:
Expr
Source
typedLambdaCalculus.scala
def toRawAsciiString: String

Attributes

Inherited from:
Expr
Source
typedLambdaCalculus.scala
def toRawString: String

Attributes

Inherited from:
Expr
Source
typedLambdaCalculus.scala
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).

Attributes

Inherited from:
Expr
Source
typedLambdaCalculus.scala
override 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.

Attributes

Definition Classes
Expr -> Any
Inherited from:
Expr
Source
typedLambdaCalculus.scala
def toUntypedAsciiString(implicit sig: BabelSignature): String

Attributes

Inherited from:
Expr
Source
typedLambdaCalculus.scala
def toUntypedString(implicit sig: BabelSignature): String

Attributes

Inherited from:
Expr
Source
typedLambdaCalculus.scala
def ty: Ty

Type of this expression (e.g. i>i>o).

Type of this expression (e.g. i>i>o).

Attributes

Inherited from:
Expr
Source
typedLambdaCalculus.scala
def |(that: Expr): Formula

Attributes

Inherited from:
Expr
Source
typedLambdaCalculus.scala
Generated with