Add doc comment and deprecation warning for Float

norm2782 · Nov 26, 2015 · adc7148 · adc7148
1 parent 140d06a
commit adc7148
Showing 1 changed file with 3 additions and 1 deletion.
diff --git a/libs/prelude/Builtins.idr b/libs/prelude/Builtins.idr
@@ -152,9 +152,11 @@ public %assert_total
 really_believe_me : a -> b
 really_believe_me x = prim__believe_me _ _ x
 
--- Deprecated - for backward compatibility
+||| Alias for `Double`. Idris does not support 32 bit floats at
+||| present.
 Float : Type
 Float = Double
+%deprecate Float
 
 -- Pointers as external primitive; there's no literals for these, so no
 -- need for them to be part of the compiler.