@@ -16,14 +16,14 @@
1616 ```
1717 [PlusNatSemi] Semigroup Nat where
1818 (<+>) x y = x + y
19−
19+
2020 [MultNatSemi] Semigroup Nat where
2121 (<+>) x y = x * y
22−
22+
2323 -- use PlusNatSemi as the parent implementation
2424 [PlusNatMonoid] Monoid Nat using PlusNatSemi where
2525 neutral = 0
26−
26+
2727 -- use MultNatSemi as the parent implementation
2828 [MultNatMonoid] Monoid Nat using MultNatSemi where
2929 neutral = 1
@@ -107,6 +107,12 @@
107107 not, leading to a contradiction. The new fine-grained equality
108108 prevents this.
109109
110+* Naming conventions for Idris packages in an iPKG file now follow the
111+ same rules for executables. Unquoted names must be valid namespaced
112+ Idris identifiers e.g. ``package my.first.package``. Quoted package
113+ names allow for packages to be given valid file names, for example,
114+ ``package "my-first-package"``.
115+
110116## Reflection changes
111117
112118* The implicit coercion from String to TTName was removed.
@@ -278,7 +284,7 @@
278284 package names that the idris project depends on. This reduces bloat in the
279285 `opts` option with multiple package declarations.
280286* iPKG files now allow `executable = "your filename here"` in addition to the
281− existing `executable = yourFilenameHere` style. While the unquoted version is
287+ Existing `Executable = yourFilenameHere` style. While the unquoted version is
282288 limited to filenames that look like namespaced Idris identifiers
283289 (`your.filename.here`), the quoted version accepts any valid filename.
284290* Add definition command (`\d` in Vim, `Ctrl-Alt-A` in Atom, `C-c C-s` in Emacs)