sig
  val ( + ) : Wp.Lang.F.binop
  val ( - ) : Wp.Lang.F.binop
  val ( ~- ) : Wp.Lang.F.unop
  val ( * ) : Wp.Lang.F.binop
  val ( / ) : Wp.Lang.F.binop
  val ( mod ) : Wp.Lang.F.binop
  val ( = ) : Wp.Lang.F.cmp
  val ( < ) : Wp.Lang.F.cmp
  val ( > ) : Wp.Lang.F.cmp
  val ( <= ) : Wp.Lang.F.cmp
  val ( >= ) : Wp.Lang.F.cmp
  val ( <> ) : Wp.Lang.F.cmp
  val ( && ) : Wp.Lang.F.operator
  val ( || ) : Wp.Lang.F.operator
  val not : Wp.Lang.F.pred -> Wp.Lang.F.pred
  val ( $ ) : Wp.Lang.lfun -> Wp.Lang.F.term list -> Wp.Lang.F.term
  val ( $$ ) : Wp.Lang.lfun -> Wp.Lang.F.term list -> Wp.Lang.F.pred
end