@@ -28,7 +28,7 @@ for use in production would be very welcome - this includes (but is not
2828limited to) extra library support, polishing the run-time system (and ensuring
2929it is robust), providing and maintaining a JVM back end, etc.
3030
31−Why does Idris use eager evaluation rather than lazy?
31+Why does Idris use eager evaluation rather than lazy?
3232-----------------------------------------------------
3333
3434Idris uses eager evaluation for more predictable performance, in particular
@@ -110,14 +110,31 @@ Does Idris have Universe Polymorphism? What is the type of ``Type``?
110110--------------------------------------------------------------------
111111
112112Rather than Universe polymorphism, Idris has a cumulative hierarchy of
113−universes; ``Type : Type 1``, ``Type 1 : Type 2``, etc.
114−Cumulativity means that if ``x : Type n`` then also ``x : Type m``,
113+universes; ``Type : Type 1``, ``Type 1 : Type 2``, etc.
114+Cumulativity means that if ``x : Type n`` then also ``x : Type m``,
115115provided that ``n <= m``.
116116
117+Why does Idris use ``Float`` and ``Double`` instead of ``Float32`` and ``Float64``?
118+------------------------------------------------------------------------------------
119+
120+Historically the C language and many other languages have used the
121+names ``Float`` and ``Double`` to represent floating point numbers of
122+size 32 and 64 respectivly. Newer languages such as Rust and Julia
123+have begun to follow the naming scheme described in `IEE Standard for
124+Floating-Point Arithmetic (IEEE 754)
125+<http://en.wikipedia.org/wiki/IEEE_floating_point>`_. This describes
126+single and double precision numbers as ``Float32`` and ``Float64``;
127+the size is described in the type name.
128+
129+Due to developer familiarity with the older naming convention, and
130+choice by the developers of Idris, Idris uses the C style convention.
131+That is, the names ``Float`` and ``Double`` are used to describe
132+single and double precision numbers.
133+
117134What does the name ‘Idris’ mean?
118135--------------------------------
119136
120−British people of a certain age may be familiar with this
137+British people of a certain age may be familiar with this
121138`singing dragon <https://www.youtube.com/watch?v=G5ZMNyscPcg>`_. If
122139that doesn’t help, maybe you can invent a suitable acronym :-) .
123140
@@ -127,4 +144,3 @@ Where can I find more answers?
127144There is an `Unofficial FAQ
128145<https://github.com/idris-lang/Idris-dev/wiki/Unofficial-FAQ>`_ on the wiki on
129146github which answers more technical questions and may be updated more often.
130−