mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-11-13 05:48:39 +03:00
Mention %access specifically
(The first failure I got when trying to compile Idris 1.3.1 code with Idris2.)
This commit is contained in:
parent
7e23c844a8
commit
38876800ca
@ -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