why3 1.3.2 · OCaml Package

type mpfr_float

exception Not_Implemented

val set_emin : int -> unit

val set_emax : int -> unit

val set_default_prec : int -> unit

type mpfr_rnd_t =

type sign =

val add : 
  ?rnd:mpfr_rnd_t ->
  ?prec:int ->
  mpfr_float ->
  mpfr_float ->
  mpfr_float

val neg : ?rnd:mpfr_rnd_t -> ?prec:int -> mpfr_float -> mpfr_float

val mul : 
  ?rnd:mpfr_rnd_t ->
  ?prec:int ->
  mpfr_float ->
  mpfr_float ->
  mpfr_float

val div : 
  ?rnd:mpfr_rnd_t ->
  ?prec:int ->
  mpfr_float ->
  mpfr_float ->
  mpfr_float

val sqrt : ?rnd:mpfr_rnd_t -> ?prec:int -> mpfr_float -> mpfr_float

val sub : 
  ?rnd:mpfr_rnd_t ->
  ?prec:int ->
  mpfr_float ->
  mpfr_float ->
  mpfr_float

val abs : ?rnd:mpfr_rnd_t -> ?prec:int -> mpfr_float -> mpfr_float

val fma : 
  ?rnd:mpfr_rnd_t ->
  ?prec:int ->
  mpfr_float ->
  mpfr_float ->
  mpfr_float ->
  mpfr_float

val rint : ?rnd:mpfr_rnd_t -> ?prec:int -> mpfr_float -> mpfr_float

val exp : ?rnd:mpfr_rnd_t -> ?prec:int -> mpfr_float -> mpfr_float

val log : ?rnd:mpfr_rnd_t -> ?prec:int -> mpfr_float -> mpfr_float

val min : 
  ?rnd:mpfr_rnd_t ->
  ?prec:int ->
  mpfr_float ->
  mpfr_float ->
  mpfr_float

val max : 
  ?rnd:mpfr_rnd_t ->
  ?prec:int ->
  mpfr_float ->
  mpfr_float ->
  mpfr_float

val signbit : mpfr_float -> sign

val subnormalize : ?rnd:mpfr_rnd_t -> mpfr_float -> mpfr_float

val make_from_str : 
  ?prec:int ->
  ?rnd:mpfr_rnd_t ->
  ?base:int ->
  string ->
  mpfr_float

val make_from_int : ?prec:int -> ?rnd:mpfr_rnd_t -> int -> mpfr_float

val make_zero : ?prec:int -> sign -> mpfr_float

val get_formatted_str : 
  ?rnd:mpfr_rnd_t ->
  ?base:int ->
  ?size:int ->
  mpfr_float ->
  string

val greater_p : mpfr_float -> mpfr_float -> bool

val greaterequal_p : mpfr_float -> mpfr_float -> bool

val less_p : mpfr_float -> mpfr_float -> bool

val lessequal_p : mpfr_float -> mpfr_float -> bool

val equal_p : mpfr_float -> mpfr_float -> bool

val lessgreater_p : mpfr_float -> mpfr_float -> bool

val zero_p : mpfr_float -> bool

val nan_p : mpfr_float -> bool

val inf_p : mpfr_float -> bool

val const_pi : ?rnd:mpfr_rnd_t -> int -> mpfr_float

package why3