formula language
declarations
sigdecl ::= sig sig { type { type , } state { compdecl } }
compdecl ::= set : expr mult | relation : expr mult -> expr mult
mult ::= ! | ? | +
expressions
expr ::= set | type | relation | expr + expr | expr & expr | expr - expr | expr . expr | ~ expr | * expr | + expr | { v | formula }
formulas
formula ::= expr = expr | expr in expr | all v | formula | some v | formula | ! formula | formula && formula
| let v be expr | formula