module AdditionSqrtSingle
  use real.RealInfix
  use real.Abs
  use ufloat.USingle
  use ufloat.USingleLemmas
  use ieee_float.RoundingMode
  use real.Square

  val function usqrt (x:usingle) : usingle

  let add_sqrt (a b : usingle)
    ensures {
      let exact = (to_real a +. to_real (usqrt b)) in
      abs (to_real result -. exact) <=. eps *. abs exact
    }
  = a ++. usqrt b
end

module AdditionSqrtDouble
  use real.RealInfix
  use real.Abs
  use ufloat.UDouble
  use ufloat.UDoubleLemmas
  use ieee_float.RoundingMode
  use real.Square

  val function usqrt (x:udouble) : udouble

  let add_sqrt (a b : udouble)
    ensures {
      let exact = (to_real a +. to_real (usqrt b)) in
      abs (to_real result -. exact) <=. eps *. abs exact
    }
  = a ++. usqrt b
end
