Docstring update for Float
This makes its status more clear.
commitb4abe259d319ea9f18a429cd21d09e4163d8c644
authorDavid Raymond Christiansen <david@davidchristiansen.dk>
dateFri 27 Nov 2015, 12:32 (11 years ago)
parent7cd0989
libs/prelude/Builtins.idr+2−2
@@ -152,8 +152,8 @@ public %assert_total
152152really_believe_me : a -> b
153153really_believe_me x = prim__believe_me _ _ x
154154
155−||| Alias for `Double`. Idris does not support 32 bit floats at
156−||| present.
155+||| Deprecated alias for `Double`, for the purpose of backwards
156+||| compatibility. Idris does not support 32 bit floats at present.
157157Float : Type
158158Float = Double
159159%deprecate Float