Add doc comment and deprecation warning for Float
commitadc7148daef90d6bb89f539f95ee7aeea5886672
authorEcho Nolan <echo@echonolan.net>
dateSat 14 Nov 2015, 13:49 (11 years ago)
parent140d06a
libs/prelude/Builtins.idr+3−1
@@ -152,9 +152,11 @@ public %assert_total
152152really_believe_me : a -> b
153153really_believe_me x = prim__believe_me _ _ x
154154
155−-- Deprecated - for backward compatibility
155+||| Alias for `Double`. Idris does not support 32 bit floats at
156+||| present.
156157Float : Type
157158Float = Double
159+%deprecate Float
158160
159161-- Pointers as external primitive; there's no literals for these, so no
160162-- need for them to be part of the compiler.