Skip to content

Commit

Permalink
FStar.Real: remove mistakenly-added to_string
Browse files Browse the repository at this point in the history
Thanks @gebner
  • Loading branch information
mtzguido committed Apr 15, 2024
1 parent 8add8b1 commit f5066f7
Showing 1 changed file with 1 addition and 3 deletions.
4 changes: 1 addition & 3 deletions ulib/FStar.Real.fsti
Original file line number Diff line number Diff line change
Expand Up @@ -25,16 +25,14 @@ module FStar.Real
This is only a logical model of the reals. There is no extraction
for them, as they are an erasable type. Any operation that can observe
a real (comparisons, to_string, etc) must be Ghost or a proposition.
a real (comparisons, etc) must be Ghost or a proposition.
*)

[@@erasable]
val real : Type0

val of_int : int -> Tot real

val to_string: real -> GTot string

val ( +. ) : real -> real -> Tot real
val ( -. ) : real -> real -> Tot real
val ( *. ) : real -> real -> Tot real
Expand Down

0 comments on commit f5066f7

Please sign in to comment.