module N:sig..end
simpler notation for writing Wp.Lang.F.term and
val (+) : Wp.Lang.F.binopF.p_add
val (-) : Wp.Lang.F.binopF.p_sub
val (~-) : Wp.Lang.F.unopfun x -> p_sub 0 x
val ( * ) : Wp.Lang.F.binopF.p_mul
val (/) : Wp.Lang.F.binopF.p_div
val (mod) : Wp.Lang.F.binopF.p_mod
val (=) : Wp.Lang.F.cmp
val (<) : Wp.Lang.F.cmp
val (>) : Wp.Lang.F.cmpWp.Lang.F.p_lt with inversed argument
val (<=) : Wp.Lang.F.cmp
val (>=) : Wp.Lang.F.cmpWp.Lang.F.p_leq with inversed argument
val (<>) : Wp.Lang.F.cmp
val (==>) : Wp.Lang.F.operator
val (&&) : Wp.Lang.F.operator
val (||) : Wp.Lang.F.operator
val not : Wp.Lang.F.pred -> Wp.Lang.F.pred
val ($) : ?result:Wp.Lang.tau -> 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