Definition float (r : R) :=
  JsonFloat.
