let test_gt1 = assert (~ (1.0R >. 2.0R))
let test_gt1 =
assert (~(1.0R >. 2.0R))
FStar.Real.fsti.checked
prims.fst.checked FStar.Pervasives.fsti.checked
FStar.Real.fsti
Prims._assert Prims.l_not Prims.b2t FStar.Real.op_Greater_Dot
(*
   Copyright 2008-2019 Microsoft Research

   Licensed under the Apache License, Version 2.0 (the "License");
   you may not use this file except in compliance with the License.
   You may obtain a copy of the License at

       http://www.apache.org/licenses/LICENSE-2.0

   Unless required by applicable law or agreed to in writing, software
   distributed under the License is distributed on an "AS IS" BASIS,
   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
   See the License for the specific language governing permissions and
   limitations under the License.
*)
module FStar.Real
(*
  This module provides a signature for real arithmetic.

  Real number constants can be specific in floating point format with
  an 'R' suffix, e.g., 1.0R

  All these operations are mapped to the corresponding primitives
  in Z3's theory of real arithmetic.
*)

val real : eqtype

val of_int : int -> Tot real

(**
  Used to extract real constants; this function is
  uninterpreted logically. i.e., 1.1R is extracted to
  [of_string "1.1"]
  *)
val of_string: string -> Tot real

val ( +. ) : real -> real -> Tot real
val ( -. ) : real -> real -> Tot real
val ( *. ) : real -> real -> Tot real
val ( /. ) : real -> d:real{d <> 0.0R} -> Tot real

val ( >.  ) : real -> real -> Tot bool
val ( >=. ) : real -> real -> Tot bool

val ( <.  ) : real -> real -> Tot bool
val ( <=. ) : real -> real -> Tot bool

#reset-options "--smtencoding.elim_box true --smtencoding.l_arith_repr native --smtencoding.nl_arith_repr native"
//Tests
let zero : real = of_int 0
let one : real = of_int 1
let two : real = of_int 2

val sqrt_2 : r:real{r *. r = two}

let n_over_n2 (n:real{n <> 0.0R /\ n*.n <> 0.0R}) = assert (n /. (n *. n) == 1.0R /. n)

let test = assert (two >. one)
let test1 = assert (one = 1.0R)

let test_lt1 = assert (1.0R <. 2.0R)
let test_lt2 = assert (~ (1.0R <. 1.0R))
let test_lt3 = assert (~ (2.0R <. 1.0R))

let test_le1 = assert (1.0R <=. 2.0R)
let test_le2 = assert (1.0R <=. 1.0R)
let test_le3 = assert (~ (2.0R <=. 1.0R))
val test_gt1 : Prims.unit
Prims.unit