Inductive float64T : Set := Float64 {
  f64 : R
}.
