@@ -187,13 +187,16 @@ It’s not a priority, though not a bad idea in the long run. It would be a
187worthwhile effort in the short term to implement libraries to support
187worthwhile effort in the short term to implement libraries to support
188self-hosting, such as a good parsing library.
188self-hosting, such as a good parsing library.
190−Does Idris have Universe Polymorphism? What is the type of ``Type``?
190+Does Idris have universe polymorphism? What is the type of ``Type``?
191====================================================================
191====================================================================
193−Rather than Universe polymorphism, Idris has a cumulative hierarchy of
193+Rather than universe polymorphism, Idris has a cumulative hierarchy of
194universes; ``Type : Type 1``, ``Type 1 : Type 2``, etc.
194universes; ``Type : Type 1``, ``Type 1 : Type 2``, etc.
195−Cumulativity means that if ``x : Type n`` then also ``x : Type m``,
195+Cumulativity means that if ``x : Type n`` and ``n <= m``, then
196−provided that ``n <= m``.
196+``x : Type m``. Universe levels are always inferred by Idris, and
197+cannot be specified explicitly. The REPL command ``:type Type 1`` will
198+result in an errror, as will attempting to specify the universe level
198Why does Idris use ``Float`` and ``Double`` instead of ``Float32`` and ``Float64``?
201Why does Idris use ``Float`` and ``Double`` instead of ``Float32`` and ``Float64``?
199===================================================================================
202===================================================================================