mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-25 04:33:45 +03:00
Merge pull request #165 from stephen-smith/docs-updates
Documentation Updates based on my first experiences with Idris 2
This commit is contained in:
commit
c3ed22c82f
@ -64,7 +64,7 @@ and is not required at run-time, as explicitly stated in the types of
|
||||
These use an ``auto``-implicit to pass around
|
||||
a ``State`` with the relevant ``tag`` implicitly, so we refer
|
||||
to states by tag alone. In ``helloCount`` earlier, we used an empty type
|
||||
\texttt{Counter} as the tag:
|
||||
``Counter`` as the tag:
|
||||
|
||||
.. code-block:: idris
|
||||
|
||||
|
@ -40,9 +40,11 @@ follows::
|
||||
|
||||
make bootstrap-racket
|
||||
|
||||
This will, by default, install into ``${HOME}/.idris2``. You can change this
|
||||
by editing the options in ``config.mk``. For example,
|
||||
to install into ``/usr/local``, you can edit the ``PREFIX`` as follows::
|
||||
Once you've successfully bootstrapped with any of the above commands, you can
|
||||
install with the command ``make install``. This will, by default, install into
|
||||
``${HOME}/.idris2``. You can change this by editing the options in
|
||||
``config.mk``. For example, to install into ``/usr/local``, you can edit the
|
||||
``PREFIX`` as follows::
|
||||
|
||||
PREFIX ?= /usr/local
|
||||
|
||||
|
@ -334,6 +334,9 @@ There are several ``%language`` pragmas in Idris 1, which define various
|
||||
experimental extensions. None of these are available in Idris 2, although
|
||||
extensions may be defined in the future.
|
||||
|
||||
Also removed was the ``%access`` pragma for default visibility, use visibility
|
||||
modifiers on each declaration instead.
|
||||
|
||||
``let`` bindings
|
||||
----------------
|
||||
|
||||
|
Loading…
Reference in New Issue
Block a user