|
1 | | -Version 1.7 |
2 | | -=========== |
| 1 | +Version 1.7.1 |
| 2 | +============= |
3 | 3 |
|
4 | 4 | The library has been tested using Agda 2.6.2. |
5 | 5 |
|
6 | | -Highlights |
7 | | ----------- |
8 | | - |
9 | | -* New module for making system calls during type checking, `Reflection.External`, |
10 | | - which re-exports `Agda.Builtin.Reflection.External`. |
11 | | - |
12 | | -* New predicate for lists that are enumerations their type in |
13 | | - `Data.List.Relation.Unary.Enumerates`. |
14 | | - |
15 | | -* New weak induction schemes in `Data.Fin.Induction` that allows one to avoid |
16 | | - the complicated use of `Acc`/`inject`/`raise` when proving inductive properties |
17 | | - over finite sets. |
18 | | - |
19 | | -Bug-fixes |
20 | | ---------- |
21 | | - |
22 | | -* Added missing module `Function.Metric` which re-exports |
23 | | - `Function.Metric.(Core/Definitions/Structures/Bundles)`. This module was referred |
24 | | - to in the documentation of its children but until now was not present. |
25 | | - |
26 | | -* Added missing fixity declaration to `_<_` in |
27 | | - `Relation.Binary.Construct.NonStrictToStrict`. |
28 | | - |
29 | | -Non-backwards compatible changes |
30 | | --------------------------------- |
31 | | - |
32 | | -#### Floating-point arithmetic |
33 | | - |
34 | | -* The functions in `Data.Float.Base` were updated following changes upstream, |
35 | | - in `Agda.Builtin.Float`, see <https://github.com/agda/agda/pull/4885>. |
36 | | - |
37 | | -* The bitwise binary relations on floating-point numbers (`_<_`, `_≈ᵇ_`, `_==_`) |
38 | | - have been removed without replacement, as they were deeply unintuitive, |
39 | | - e.g., `∀ x → x < -x`. |
40 | | - |
41 | | -#### Reflection |
42 | | - |
43 | | -* The representation of reflected syntax in `Reflection.Term`, |
44 | | - `Reflection.Pattern`, `Reflection.Argument` and |
45 | | - `Reflection.Argument.Information` has been updated to match the new |
46 | | - representation used in Agda 2.6.2. Specifically, the following |
47 | | - changes were made: |
48 | | - |
49 | | - * The type of the `var` constructor of the `Pattern` datatype has |
50 | | - been changed from `(x : String) → Pattern` to `(x : Int) → |
51 | | - Pattern`. |
52 | | - |
53 | | - * The type of the `dot` constructor of the `Pattern` datatype has |
54 | | - been changed from `Pattern` to `(t : Term) → Pattern`. |
55 | | - |
56 | | - * The types of the `clause` and `absurd-clause` constructors of the |
57 | | - `Clause` datatype now take an extra argument `(tel : Telescope)`, |
58 | | - where `Telescope = List (String × Arg Type)`. |
59 | | - |
60 | | - * The following constructors have been added to the `Sort` datatype: |
61 | | - `prop : (t : Term) → Sort`, `propLit : (n : Nat) → Sort`, and |
62 | | - `inf : (n : Nat) → Sort`. |
63 | | - |
64 | | - * In `Reflection.Argument.Information` the function `relevance` was |
65 | | - replaced by `modality`. |
66 | | - |
67 | | - * The type of the `arg-info` constructor is now |
68 | | - `(v : Visibility) (m : Modality) → ArgInfo`. |
69 | | - |
70 | | - * In `Reflection.Argument` (as well as `Reflection`) there is a new |
71 | | - pattern synonym `defaultModality`, and the pattern synonyms |
72 | | - `vArg`, `hArg` and `iArg` have been changed. |
73 | | - |
74 | | - * Two new modules have been added, `Reflection.Argument.Modality` |
75 | | - and `Reflection.Argument.Quantity`. The constructors of the types |
76 | | - `Modality` and `Quantity` are reexported from `Reflection`. |
77 | | - |
78 | | -#### Sized types |
79 | | - |
80 | | -* Sized types are no longer considered safe in Agda 2.6.2. As a |
81 | | - result, all modules that use `--sized-types` no longer have the |
82 | | - `--safe` flag. For a full list of affected modules, refer to the |
83 | | - relevant [commit](https://github.com/agda/agda-stdlib/pull/1465/files#diff-e1c0e3196e4cea6ff808f5d2906031a7657130e10181516206647b83c7014584R91-R131.) |
84 | | - |
85 | | -* In order to maintain the safety of `Data.Nat.Pseudorandom.LCG`, the function |
86 | | - `stream` that relies on the newly unsafe `Codata` modules has |
87 | | - been moved to the new module `Data.Nat.Pseudorandom.LCG.Unsafe`. |
88 | | - |
89 | | -* In order to maintain the safety of the modules in the `Codata.Musical` directory, |
90 | | - the functions `fromMusical` and `toMusical` defined in: |
91 | | - ``` |
92 | | - Codata.Musical.Colist |
93 | | - Codata.Musical.Conat |
94 | | - Codata.Musical.Cofin |
95 | | - Codata.Musical.M |
96 | | - Codata.Musical.Stream |
97 | | - ``` |
98 | | - have been moved to a new module `Codata.Musical.Conversion` and renamed to |
99 | | - `X.fromMusical` and `X.toMusical` for each of `Codata.Musical.X`. |
100 | | - |
101 | | -* In order to maintain the safety of `Data.Container(.Indexed)`, the greatest fixpoint |
102 | | - of containers, `ν`, has been moved from `Data.Container(.Indexed)` to a new module |
103 | | - `Data.Container(.Indexed).Fixpoints.Guarded` which also re-exports the least fixpoint. |
104 | | - |
105 | | -#### Other |
106 | | - |
107 | | -* Replaced existing O(n) implementation of `Data.Nat.Binary.fromℕ` with a new O(log n) |
108 | | - implementation. The old implementation is maintained under `Data.Nat.Binary.fromℕ'` |
109 | | - and proven to be equivalent to the new one. |
110 | | - |
111 | | -* `Data.Maybe.Base` now re-exports the definition of `Maybe` given by |
112 | | - `Agda.Builtin.Maybe`. The `Foreign.Haskell` modules and definitions |
113 | | - corresponding to `Maybe` have been removed. See the release notes of |
114 | | - Agda 2.6.2 for more information. |
115 | | - |
116 | | -Deprecated modules |
117 | | ------------------- |
118 | | - |
119 | | -Deprecated names |
120 | | ----------------- |
121 | | - |
122 | | -New modules |
123 | | ------------ |
124 | | - |
125 | | -* New module for making system calls during type checking: |
126 | | - ```agda |
127 | | - Reflection.External |
128 | | - ``` |
129 | | - |
130 | | -* New modules for universes and annotations of reflected syntax: |
131 | | - ``` |
132 | | - Reflection.Universe |
133 | | - Reflection.Annotated |
134 | | - Reflection.Annotated.Free |
135 | | - ``` |
136 | | - |
137 | | -* Added new module for unary relations over sized types now that `Size` |
138 | | - lives in it's own universe since Agda 2.6.2. |
139 | | - ```agda |
140 | | - Relation.Unary.Sized |
141 | | - ``` |
142 | | - |
143 | | -* Metrics specialised to co-domains with rational numbers: |
144 | | - ``` |
145 | | - Function.Metric.Rational |
146 | | - Function.Metric.Rational.Definitions |
147 | | - Function.Metric.Rational.Structures |
148 | | - Function.Metric.Rational.Bundles |
149 | | - ``` |
150 | | - |
151 | | -* Lists that contain every element of a type: |
152 | | - ``` |
153 | | - Data.List.Relation.Unary.Enumerates.Setoid |
154 | | - Data.List.Relation.Unary.Enumerates.Setoid.Properties |
155 | | - ``` |
156 | | - |
157 | | -* (Unsafe) sized W type: |
158 | | - ``` |
159 | | - Data.W.Sized |
160 | | - ``` |
161 | | - |
162 | | -* (Unsafe) container fixpoints: |
163 | | - ``` |
164 | | - Data.Container.Fixpoints.Sized |
165 | | - ``` |
166 | | - |
167 | | -Other minor additions |
168 | | ---------------------- |
169 | | - |
170 | | -* Added new relations to `Data.Fin.Base`: |
171 | | - ```agda |
172 | | - _≥_ = ℕ._≥_ on toℕ |
173 | | - _>_ = ℕ._>_ on toℕ |
174 | | - ``` |
175 | | - |
176 | | -* Added new proofs to `Data.Fin.Induction`: |
177 | | - ```agda |
178 | | - >-wellFounded : WellFounded {A = Fin n} _>_ |
179 | | -
|
180 | | - <-weakInduction : P zero → (∀ i → P (inject₁ i) → P (suc i)) → ∀ i → P i |
181 | | - >-weakInduction : P (fromℕ n) → (∀ i → P (suc i) → P (inject₁ i)) → ∀ i → P i |
182 | | - ``` |
183 | | - |
184 | | -* Added new proofs to `Relation.Binary.Properties.Setoid`: |
185 | | - ```agda |
186 | | - respʳ-flip : _≈_ Respectsʳ (flip _≈_) |
187 | | - respˡ-flip : _≈_ Respectsˡ (flip _≈_) |
188 | | - ``` |
189 | | - |
190 | | -* Added new function to `Data.Fin.Base`: |
191 | | - ```agda |
192 | | - pinch : Fin n → Fin (suc n) → Fin n |
193 | | - ``` |
194 | | - |
195 | | -* Added new proofs to `Data.Fin.Properties`: |
196 | | - ```agda |
197 | | - pinch-surjective : Surjective _≡_ (pinch i) |
198 | | - pinch-mono-≤ : (pinch i) Preserves _≤_ ⟶ _≤_ |
199 | | - ``` |
200 | | - |
201 | | -* Added new proofs to `Data.Nat.Binary.Properties`: |
202 | | - ```agda |
203 | | - fromℕ≡fromℕ' : fromℕ ≗ fromℕ' |
204 | | - toℕ-fromℕ' : toℕ ∘ fromℕ' ≗ id |
205 | | - fromℕ'-homo-+ : fromℕ' (m ℕ.+ n) ≡ fromℕ' m + fromℕ' n |
206 | | - ``` |
207 | | - |
208 | | -* Rewrote proofs in `Data.Nat.Binary.Properties` for new implementation of `fromℕ`: |
209 | | - ```agda |
210 | | - toℕ-fromℕ : toℕ ∘ fromℕ ≗ id |
211 | | - fromℕ-homo-+ : fromℕ (m ℕ.+ n) ≡ fromℕ m + fromℕ n |
212 | | - ``` |
213 | | - |
214 | | -* Added new proof to `Data.Nat.DivMod`: |
215 | | - ```agda |
216 | | - m/n≤m : (m / n) {≢0} ≤ m |
217 | | - ``` |
218 | | - |
219 | | -* Added new type in `Size`: |
220 | | - ```agda |
221 | | - SizedSet ℓ = Size → Set ℓ |
222 | | - ``` |
| 6 | +* The only change over v1.7 is that the library's Cabal file is now compatible with GHC 9.2. |
0 commit comments