Skip to main content

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.


Receive important developer updates