update changelog and documentation

idris-lang · Jul 11, 2023 · 7c34a08 · 7c34a08
1 parent dcdb6e1
commit 7c34a08
Show file tree

Hide file tree

Showing 2 changed files with 10 additions and 0 deletions.
diff --git a/CHANGELOG.md b/CHANGELOG.md
@@ -16,6 +16,7 @@
 * Rudimentary support for defining lazy functions (addressing issue
   [#1066](https://github.com/idris-lang/idris2/issues/1066)).
 * `%hide` directives can now hide conflicting fixities from other modules.
+* Fixity declarations can now be kept private with export modifiers.
 
 ### REPL changes
 

diff --git a/docs/source/tutorial/modules.rst b/docs/source/tutorial/modules.rst
@@ -162,6 +162,15 @@ For interfaces, the meanings are:
 - ``public export`` the interface name, method names and default
   definitions are exported
 
+Meaning for fixity declarations
+-------------------------------
+
+For fixity declarations:
+
+- ``private`` means the fixity declaration is only valid within the file.
+
+- ``public export`` and ``export`` are the same and the fixity is exported.
+
 Propagating Inner Module API's
 -------------------------------