git.iko.soy/Idris-dev
on master help sign in
use `Double` instead of `Float` in docs
0e5a476zjhmale
docs/faq/faq.rst+3−3
compare with master
unifiedsplit
@@ -198,7 +198,7 @@ cannot be specified explicitly. The REPL command ``:type Type 1`` will
198result in an error, as will attempting to specify the universe level
198result in an error, as will attempting to specify the universe level
199of any type.
199of any type.
200
200
201−Why does Idris use ``Float`` and ``Double`` instead of ``Float32`` and ``Float64``?
201+Why does Idris use ``Double`` instead of ``Float64``?
202===================================================================================
202===================================================================================
203
203
204Historically the C language and many other languages have used the
204Historically the C language and many other languages have used the
@@ -212,8 +212,8 @@ the size is described in the type name.
212
212
213Due to developer familiarity with the older naming convention, and
213Due to developer familiarity with the older naming convention, and
214choice by the developers of Idris, Idris uses the C style convention.
214choice by the developers of Idris, Idris uses the C style convention.
215−That is, the names ``Float`` and ``Double`` are used to describe
215+That is, the name ``Double`` is used to describe double precision
216−single and double precision numbers.
216+numbers, and Idris does not support 32 bit floats at present.
217
217
218What is -ffreestanding?
218What is -ffreestanding?
219=======================
219=======================
docs/reference/ffi.rst+1−1
@@ -341,7 +341,7 @@ follows:
341
341
342 data JS_Types : Type -> Type where
342 data JS_Types : Type -> Type where
343 JS_Str : JS_Types String
343 JS_Str : JS_Types String
344− JS_Float : JS_Types Float
344+ JS_Float : JS_Types Double
345 JS_Ptr : JS_Types Ptr
345 JS_Ptr : JS_Types Ptr
346 JS_Unit : JS_Types ()
346 JS_Unit : JS_Types ()
347 JS_FnT : JS_FnTypes a -> JS_Types (JsFn a)
347 JS_FnT : JS_FnTypes a -> JS_Types (JsFn a)
docs/reference/repl.rst+1−1
@@ -367,7 +367,7 @@ some string, and prints the results. For example:
367
367
368 prim__eqChar : Char -> Char -> Int
368 prim__eqChar : Char -> Char -> Int
369
369
370− prim__eqFloat : Float -> Float -> Int
370+ prim__eqFloat : Double -> Double -> Int
371
371
372 prim__eqInt : Int -> Int -> Int
372 prim__eqInt : Int -> Int -> Int
373
373
docs/tutorial/interfaces.rst+1−1
@@ -6,7 +6,7 @@ Interfaces
6
6
7We often want to define functions which work across several different
7We often want to define functions which work across several different
8data types. For example, we would like arithmetic operators to work on
8data types. For example, we would like arithmetic operators to work on
9−``Int``, ``Integer`` and ``Float`` at the very least. We would like
9+``Int``, ``Integer`` and ``Double`` at the very least. We would like
10``==`` to work on the majority of data types. We would like to be able
10``==`` to work on the majority of data types. We would like to be able
11to display different types in a uniform way.
11to display different types in a uniform way.
12
12
docs/tutorial/miscellany.rst+2−2
@@ -151,7 +151,7 @@ function:
151
151
152 interpFTy : FTy -> Type
152 interpFTy : FTy -> Type
153 interpFTy FInt = Int
153 interpFTy FInt = Int
154− interpFTy FFloat = Float
154+ interpFTy FFloat = Double
155 interpFTy FChar = Char
155 interpFTy FChar = Char
156 interpFTy FString = String
156 interpFTy FString = String
157 interpFTy FPtr = Ptr
157 interpFTy FPtr = Ptr
@@ -237,7 +237,7 @@ command or the ``%dynamic`` directive. For example:
237
237
238 Idris> :dynamic libm.so
238 Idris> :dynamic libm.so
239 Idris> :x unsafePerformIO ((mkForeign (FFun "sin" [FFloat] FFloat)) 1.6)
239 Idris> :x unsafePerformIO ((mkForeign (FFun "sin" [FFloat] FFloat)) 1.6)
240− 0.9995736030415051 : Float
240+ 0.9995736030415051 : Double
241
241
242Type Providers
242Type Providers
243==============
243==============
docs/tutorial/syntax.rst+1−1
@@ -73,7 +73,7 @@ bound is below the upper bound using ``so``:
73.. code-block:: idris
73.. code-block:: idris
74
74
75 data Interval : Type where
75 data Interval : Type where
76− MkInterval : (lower : Float) -> (upper : Float) ->
76+ MkInterval : (lower : Double) -> (upper : Double) ->
77 so (lower < upper) -> Interval
77 so (lower < upper) -> Interval
78
78
79We can define a syntax which, in patterns, always matches ``oh`` for
79We can define a syntax which, in patterns, always matches ``oh`` for
docs/tutorial/typesfuns.rst+1−1
@@ -8,7 +8,7 @@ Primitive Types
8===============
8===============
9
9
10Idris defines several primitive types: ``Int``, ``Integer`` and
10Idris defines several primitive types: ``Int``, ``Integer`` and
11−``Float`` for numeric operations, ``Char`` and ``String`` for text
11+``Double`` for numeric operations, ``Char`` and ``String`` for text
12manipulation, and ``Ptr`` which represents foreign pointers. There are
12manipulation, and ``Ptr`` which represents foreign pointers. There are
13also several data types declared in the library, including ``Bool``,
13also several data types declared in the library, including ``Bool``,
14with values ``True`` and ``False``. We can declare some constants with
14with values ``True`` and ``False``. We can declare some constants with