mirror of
https://github.com/ilyakooo0/Idris-dev.git
synced 2024-09-11 08:55:23 +03:00
Update introduction.rst
Got the error `Can't find import Effects` when attempting this part of the tutorial. Managed to solve it after finding issue #1524, but would have been faster if this flag was mentioned in the tutorial.
This commit is contained in:
parent
93cfe987f3
commit
289b0589ae
@ -17,7 +17,8 @@ exceptions, and verified resource management.
|
|||||||
This tutorial assumes familiarity with pure programming in Idris,
|
This tutorial assumes familiarity with pure programming in Idris,
|
||||||
as described in Sections 1–6 of the main tutorial [1]_. The examples
|
as described in Sections 1–6 of the main tutorial [1]_. The examples
|
||||||
presented are tested with Idris and can be found in the
|
presented are tested with Idris and can be found in the
|
||||||
examples directory of the Idris repository.
|
examples directory of the Idris repository. The ``-p effects`` flag
|
||||||
|
is needed when starting Idris.
|
||||||
|
|
||||||
Consider, for example, the following introductory function which
|
Consider, for example, the following introductory function which
|
||||||
illustrates the kind of properties which can be expressed in the type
|
illustrates the kind of properties which can be expressed in the type
|
||||||
|
Loading…
Reference in New Issue
Block a user