@@ -195,7 +195,7 @@ universes; ``Type : Type 1``, ``Type 1 : Type 2``, etc.
195Cumulativity means that if ``x : Type n`` and ``n <= m``, then
195Cumulativity means that if ``x : Type n`` and ``n <= m``, then
196``x : Type m``. Universe levels are always inferred by Idris, and
196``x : Type m``. Universe levels are always inferred by Idris, and
197cannot be specified explicitly. The REPL command ``:type Type 1`` will
197cannot be specified explicitly. The REPL command ``:type Type 1`` will
198−result in an errror, as will attempting to specify the universe level
198+result in an error, as will attempting to specify the universe level
199of any type.
199of any type.
201Why does Idris use ``Float`` and ``Double`` instead of ``Float32`` and ``Float64``?
201Why does Idris use ``Float`` and ``Double`` instead of ``Float32`` and ``Float64``?