Last updated
Quantification operators
forall
pact
(forall (x:string) y) pact
(forall (x:string) y)- binds
x: a - takes
y: r - produces r
- where a is any type
- where r is any type
Bind a universally-quantified variable
Supported in properties only.
exists
pact
(exists (x:string) y) pact
(exists (x:string) y)- binds
x: a - takes
y: r - produces r
- where a is any type
- where r is any type
Bind an existentially-quantified variable
Supported in properties only.
column-of
pact
(column-of t) pact
(column-of t)- takes
t:table - produces
type
The type of columns for a given table. Commonly used in conjunction with
quantification; e.g.:
(exists (col:(column-of accounts)) (column-written accounts col)).
Supported in properties only.