data class ForAll : Formula, Binary<ForAll, Formula>
First-order forall operator. Specifies that for all states in bound substituted for name, the target formula is valid at inspected state.
Note that (forall x in A : B) is semantically equivalent to (forall x : ((at x: A) -> B)).
However, we allow the in syntax because it is much more readable and can yield interesting
performance optimisations.
Warning: name must usually be a free name (not assigned yet).
| <init> |
ForAll(name: String, bound: Formula, target: Formula)
First-order forall operator. Specifies that for all states in bound substituted for name, the target formula is valid at inspected state. |
| bound |
val bound: Formula
The bound formula which limits the states considered for substitution. |
| left |
val left: Formula
The child of this element which is the root of the left subtree. |
| name |
val name: String
The name that should be substituted in the target formula. |
| right |
val right: Formula
The child of this element which is the root of the right subtree. |
| target |
val target: Formula
The target formula which is subject to substitution. |
| node |
open val node: Formula
Formula is also the node in the tree, so |
| copy |
fun copy(left: Formula, right: Formula): ForAll
Create a copy of the original object but optionally replace the left or right child element. |
| toString |
fun toString(): String
Return string which uniquely represents this formula and can be parsed to create an equivalent object. |