parse_as_prefix "Not";;
parse_as_infix("&&",(16,"right"));;
parse_as_infix("||",(15,"right"));;
parse_as_infix("-->",(14,"right"));;
parse_as_infix("<->",(13,"right"));;

let false_def = define `False = \t:num. F`;;
let true_def = define `True = \t:num. T`;;
let not_def = define `Not p = \t:num. ~(p t)`;;
let and_def = define `p && q = \t:num. p t /\ q t`;;
let or_def = define `p || q = \t:num. p t \/ q t`;;
let imp_def = define `p --> q = \t:num. p t ==> q t`;;
let iff_def = define `p <-> q = \t:num. p t <=> q t`;;
let forever = define `forever p = \t:num. !t'. t <= t' ==> p t'`;;
let sometime = define `sometime p = \t:num. ?t'. t <= t' /\ p t'`;;
let next = define `next p = \t:num. p(t + 1)`;;
parse_as_infix("until",(17,"right"));;

let until = define
  `p until q =
    \t:num. ?t'. t <= t' /\ (!t''. t <= t'' /\ t'' < t' ==> p t'') /\ q t'`;;