HUCTLp / com.github.sybila.huctl / Formula / ForAll / <init>

<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.

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).