Toplevel definitions
Definitions in seach section of a flat specification or a modulesection  description  syntax  example 

types 
type alias 
name = type inv pattern == conditional expression; 
pair = nat * nat; pair = nat * nat inv mk_(x, y) == x + 1 = y; pair = nat * nat inv p == p.#1 + 1 = p.#2; 
record definition 
name :: fieldname:type fieldname:type... inv pattern == conditional expression; 
Point :: x:real y:real; FirstQuadrant :: x:real y:real inv mk_FirstQuadrant(x, y) == x >= 0 and y >= 0; FirstQuadrant :: x:real y:real inv p == p.x >= 0 and p.y >= 0; 

values 
constant value definition 
name : type = expression; 
PI : real = 3.141592653589793238 PI2 = PI * 2 
functions 
explicit function definition 
name: type * ... * type > type

mid : real * real > real

state 
state definition 
state statename of 
state Cursor of

operations 
pure operation definition 
pure name: type * ... * type ==> type

pure cursorColumn: () ==> nat

explicit operation definition 
name: type * ... * type ==> type

moveColumn: int ==> ()

Local definitions
kind  description  syntax  example 

expression  let expression 
let pattern:type=expression,...,pattern:type=expression in expression 
let x:nat = 1 in x + 1 let x = 1 in x + 1 let x:nat = 1, y:nat = 2 in x + y let f:nat > nat1 f(x) == x + 1 in f(2) 
let be expression (conditional matching) 
let multiple bind be st conditional expression in expression 
let x in set {1,2,3,4} be st x mod 2 = 0 in x let b1, b2:bool be st b1 => b2 in mk_(b1, b2) 

statement  let statement 
let pattern:type=expression,...,pattern:type=expression in statement 
let x:nat = 1 in return x + 1 let x = 1 in return := x + 1 let x:nat = 1, y:nat = 2 in return x + y let f:nat > nat1 f(x) == x + 1 in f(2) 
let be statement (conditional matching) 
let multiple bind be st conditional expression in statement 
let x in set {1,2,3,4} be st x mod 2 = 0 in return x let b1, b2:bool be st b1 => b2 in return mk_(b1, b2) 

block variable 
(dcl name:type=expression,...,name:type=expression; statement; ...) 
(dcl tmp:nat := v1; v1 := v2; v2 := tmp)


int for loop 
for name = integer expression to integer expression by integer expression do statement 
for i = 1 to 10 do s := s ^ [i]


sequance for loop 
for pattern in sequence expression do statement 
for i in [1,2,3,4,5] do s := s ^ [i]


set for loop 
for all pattern in set set expression do statement 
for all i in set {1,...,10} do s := s ^ [i]

Patterns
type  description  syntax  example 

any  identifier  name 
let x = 1 in x + 2 
don't care   
let  = 1 in 2 

value 
literal (expression) 
cases 4 mod 2: 0 > <odd>, 1 > <even> end 

product  tuple pattern  mk_(pattern,...,pattern) 
let mk_(x, y) = mk_(1, 2) in x + y 
record  record pattern  mk_name(pattern,...,pattern) 
let mk_Point(x, y) = mk_Point(1, 2) in x + y 
set  set enumeration pattern  {pattern,...,pattern} 
let {x, y} = {1, 2} in x + y 
set union pattern  pattern union pattern 
let {x} union {1, 3} = {1, 2, 3} in x 

seq  sequence enumeration pattern  [pattern,...,pattern] 
let [x, y] = [1, 2] in x + y 
concat pattern  pattern ^ pattern 
let x^[3] = [1,2,3] in x 

map  map enumeration pattern  [pattern > pattern,...,pattern > pattern] 
let {2 > , 1 > x} = {1 > 2, 2 > 3} in x 
map union pattern  pattern munion pattern 
let  munion {1 > x} = {1 > 2, 2 > 3} in x 
Bindings
type bind 
pattern:type 
{mk_(b1, b2)  b1, b2:bool} 
set bind  pattern in set set expression 
{mk_(b1, b2)  b1, b2 in set {true, false}} 