mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-09-11 13:36:08 +03:00
Use reST directives to make warnings and TODOs explicit in the documentation.
This commit is contained in:
parent
08e4955c0b
commit
43c5075f6e
@ -4,4 +4,6 @@
|
||||
Environment Variables
|
||||
*********************
|
||||
|
||||
[TODO: Fill in the environment variables recognised by Idris 2]
|
||||
.. todo::
|
||||
|
||||
Fill in the environment variables recognised by Idris 2
|
||||
|
@ -81,9 +81,9 @@ number as 0), we could write:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
fibonacci : {default 0 lag : Nat} -> {default 1 lead : Nat} -> (n : Nat) -> Nat
|
||||
fibonacci {lag} Z = lag
|
||||
fibonacci {lag} {lead} (S n) = fibonacci {lag=lead} {lead=lag+lead} n
|
||||
fibonacci : {default 0 lag : Nat} -> {default 1 lead : Nat} -> (n : Nat) -> Nat
|
||||
fibonacci {lag} Z = lag
|
||||
fibonacci {lag} {lead} (S n) = fibonacci {lag=lead} {lead=lag+lead} n
|
||||
|
||||
After this definition, ``fibonacci 5`` is equivalent to ``fibonacci {lag=0} {lead=1} 5``,
|
||||
and will return the 5th fibonacci number. Note that while this works, this is not the
|
||||
@ -114,7 +114,9 @@ any other character).
|
||||
Cumulativity
|
||||
============
|
||||
|
||||
[NOT YET IN IDRIS 2]
|
||||
.. warning::
|
||||
|
||||
NOT YET IN IDRIS 2
|
||||
|
||||
Since values can appear in types and *vice versa*, it is natural that
|
||||
types themselves have types. For example:
|
||||
|
@ -126,7 +126,7 @@ To see more detail on what's going on, we can replace the recursive call to
|
||||
``plusReducesZ`` with a hole:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
|
||||
plusReducesZ (S k) = cong S ?help
|
||||
|
||||
Then inspecting the type of the hole at the REPL shows us:
|
||||
@ -361,7 +361,9 @@ total, a function ``f`` must:
|
||||
Directives and Compiler Flags for Totality
|
||||
------------------------------------------
|
||||
|
||||
[NOTE: Not all of this is implemented yet for Idris 2]
|
||||
.. warning::
|
||||
|
||||
Not all of this is implemented yet for Idris 2
|
||||
|
||||
By default, Idris allows all well-typed definitions, whether total or not.
|
||||
However, it is desirable for functions to be total as far as possible, as this
|
||||
|
@ -4,7 +4,9 @@
|
||||
Views and the “``with``” rule
|
||||
*****************************
|
||||
|
||||
[NOT UPDATED FOR IDRIS 2 YET]
|
||||
.. warning::
|
||||
|
||||
NOT UPDATED FOR IDRIS 2 YET
|
||||
|
||||
Dependent pattern matching
|
||||
==========================
|
||||
|
@ -453,4 +453,6 @@ In ``ATM.idr``, add:
|
||||
Chapter 15
|
||||
----------
|
||||
|
||||
TODO
|
||||
.. todo::
|
||||
|
||||
This chapter.
|
||||
|
@ -428,8 +428,11 @@ used with care. Too many hints can lead to a large search space!
|
||||
Totality and Coverage
|
||||
---------------------
|
||||
|
||||
``%default covering`` is now the default status [Actually still TODO, but
|
||||
planned soon!]
|
||||
``%default covering`` is now the default statusk
|
||||
|
||||
.. note::
|
||||
|
||||
Actually still TODO, but planned soon!
|
||||
|
||||
Build artefacts
|
||||
---------------
|
||||
|
Loading…
Reference in New Issue
Block a user