@@ -152,9 +152,11 @@ public %assert_total
152really_believe_me : a -> b
152really_believe_me : a -> b
153really_believe_me x = prim__believe_me _ _ x
153really_believe_me x = prim__believe_me _ _ x
155−-- Deprecated - for backward compatibility
155+||| Alias for `Double`. Idris does not support 32 bit floats at
156Float : Type
157Float : Type
157Float = Double
158Float = Double
159-- Pointers as external primitive; there's no literals for these, so no
161-- Pointers as external primitive; there's no literals for these, so no
160-- need for them to be part of the compiler.
162-- need for them to be part of the compiler.