Quantification operators
forall
(forall (x:string) y)(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
(exists (x:string) y)(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
(column-of t)(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.