git.iko.soy/Idris-dev
on master help sign in
Rename Float to Double in Parser

Also add a definition in Builtins to keep the old name, temporarily, for backward compatibility.

commit89e325cf1f7e23d5484c7f41278b76d5045075c8 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSat 28 Mar 2015, 18:48 (12 years ago) parent8472966
3 files changed+8−1
compare with master
unifiedsplit
libs/prelude/Builtins.idr+5 libs/prelude/Prelude/Cast.idr+2 src/Idris/ParseExpr.hs+1−1
libs/prelude/Builtins.idr+5
@@ -149,3 +149,8 @@ believe_me x = prim__believe_me _ _ x
149149public %assert_total
150150really_believe_me : a -> b
151151really_believe_me x = prim__believe_me _ _ x
152+
153+-- Deprecated - for backward compatibility
154+Float : Type
155+Float = Double
156+
libs/prelude/Prelude/Cast.idr+2
@@ -1,5 +1,7 @@
11module Prelude.Cast
22
3+import public Builtins
4+
35||| Type class for transforming a instance of a data type to another type.
46class Cast from to where
57 ||| Perform a cast operation.
src/Idris/ParseExpr.hs+1−1
@@ -1156,7 +1156,7 @@ constants =
11561156 [ ("Integer", AType (ATInt ITBig))
11571157 , ("Int", AType (ATInt ITNative))
11581158 , ("Char", AType (ATInt ITChar))
1159− , ("Float", AType ATFloat)
1159+ , ("Double", AType ATFloat)
11601160 , ("String", StrType)
11611161 , ("Ptr", PtrType)
11621162 , ("ManagedPtr", ManagedPtrType)