module Vale.Lib.Operator

/*
Logical operators returning bool or Type0:

   bool    Type0
   ----    -----
   true    True
   false   False
   not     ! or ~
   =       ==
   <>      != or =!=
   &&      /\
   ||      \/
           ==>
           <==
   =       <==>
   <
   >
   <=
   >=

Note that <, >, <=, >= may be chained together: 0 <= i < n turns into 0 <= i && i < n
*/

#token ~ precedence !
#token <> precedence !=
#token /\ precedence &&
#token \/ precedence ||

function operator(~) (x:Type0):Type0 := l_not;
function operator(<>) (x:Type0, y:Type0):Type0 := op_disEquality;
function operator(/\) (x:Type0, y:Type0):Type0 := l_and;
function operator(\/) (x:Type0, y:Type0):Type0 := l_or;

type state:Type(0) {:primitive} := va_state;
type list(a:Type(0)):Type(0) {:primitive} := Prims.list(a);