@@ -195,7 +195,7 @@ universes; ``Type : Type 1``, ``Type 1 : Type 2``, etc.
195195Cumulativity means that if ``x : Type n`` and ``n <= m``, then
196196``x : Type m``. Universe levels are always inferred by Idris, and
197197cannot 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
199199of any type.
200200
201201Why does Idris use ``Float`` and ``Double`` instead of ``Float32`` and ``Float64``?