0e5a476 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

use `Double` instead of `Float` in docs

commit0e5a4764b3a7603a3f254c2fba75b1b0203ac2ba authorzjhmale <zjhmale@gmail.com> dateWed 27 Jul 2016, 20:06 (10 years ago) parentaa2d977

7 files changed+10−10

compare with master

unifiedsplit

docs/faq/faq.rst+3−3 docs/reference/ffi.rst+1−1 docs/reference/repl.rst+1−1 docs/tutorial/interfaces.rst+1−1 docs/tutorial/miscellany.rst+2−2 docs/tutorial/syntax.rst+1−1 docs/tutorial/typesfuns.rst+1−1

docs/faq/faq.rst+3−3

@@ -198,7 +198,7 @@ cannot be specified explicitly. The REPL command ``:type Type 1`` will

198198result in an error, as will attempting to specify the universe level

199199of any type.

200200

201−Why does Idris use ``Float`` and ``Double`` instead of ``Float32`` and ``Float64``?

201+Why does Idris use ``Double`` instead of ``Float64``?

202202===================================================================================

203203

204204Historically the C language and many other languages have used the

@@ -212,8 +212,8 @@ the size is described in the type name.

212212

213213Due to developer familiarity with the older naming convention, and

214214choice by the developers of Idris, Idris uses the C style convention.

215−That is, the names ``Float`` and ``Double`` are used to describe

216−single and double precision numbers.

215+That is, the name ``Double`` is used to describe double precision

216+numbers, and Idris does not support 32 bit floats at present.

217217

218218What is -ffreestanding?

219219=======================

docs/reference/ffi.rst+1−1

@@ -341,7 +341,7 @@ follows:

341341

342342 data JS_Types : Type -> Type where

343343 JS_Str : JS_Types String

344− JS_Float : JS_Types Float

344+ JS_Float : JS_Types Double

345345 JS_Ptr : JS_Types Ptr

346346 JS_Unit : JS_Types ()

347347 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:

367367

368368 prim__eqChar : Char -> Char -> Int

369369

370− prim__eqFloat : Float -> Float -> Int

370+ prim__eqFloat : Double -> Double -> Int

371371

372372 prim__eqInt : Int -> Int -> Int

373373

docs/tutorial/interfaces.rst+1−1

@@ -6,7 +6,7 @@ Interfaces

77We often want to define functions which work across several different

88data 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

1010``==`` to work on the majority of data types. We would like to be able

1111to display different types in a uniform way.

1212

docs/tutorial/miscellany.rst+2−2

@@ -151,7 +151,7 @@ function:

151151

152152 interpFTy : FTy -> Type

153153 interpFTy FInt = Int

154− interpFTy FFloat = Float

154+ interpFTy FFloat = Double

155155 interpFTy FChar = Char

156156 interpFTy FString = String

157157 interpFTy FPtr = Ptr

@@ -237,7 +237,7 @@ command or the ``%dynamic`` directive. For example:

237237

238238 Idris> :dynamic libm.so

239239 Idris> :x unsafePerformIO ((mkForeign (FFun "sin" [FFloat] FFloat)) 1.6)

240− 0.9995736030415051 : Float

240+ 0.9995736030415051 : Double

241241

242242Type Providers

243243==============

docs/tutorial/syntax.rst+1−1

@@ -73,7 +73,7 @@ bound is below the upper bound using ``so``:

7373.. code-block:: idris

7474

7575 data Interval : Type where

76− MkInterval : (lower : Float) -> (upper : Float) ->

76+ MkInterval : (lower : Double) -> (upper : Double) ->

7777 so (lower < upper) -> Interval

7878

7979We can define a syntax which, in patterns, always matches ``oh`` for

docs/tutorial/typesfuns.rst+1−1

@@ -8,7 +8,7 @@ Primitive Types

88===============

1010Idris 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

1212manipulation, and ``Ptr`` which represents foreign pointers. There are

1313also several data types declared in the library, including ``Bool``,

1414with values ``True`` and ``False``. We can declare some constants with