-
Notifications
You must be signed in to change notification settings - Fork 242
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
- Loading branch information
1 parent
5d459fd
commit b85c5d1
Showing
6 changed files
with
13 additions
and
233 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -1,222 +1,6 @@ | ||
| Version 1.7 | ||
| =========== | ||
| Version 1.7.1 | ||
| ============= | ||
|
|
||
| The library has been tested using Agda 2.6.2. | ||
|
|
||
| Highlights | ||
| ---------- | ||
|
|
||
| * New module for making system calls during type checking, `Reflection.External`, | ||
| which re-exports `Agda.Builtin.Reflection.External`. | ||
|
|
||
| * New predicate for lists that are enumerations their type in | ||
| `Data.List.Relation.Unary.Enumerates`. | ||
|
|
||
| * New weak induction schemes in `Data.Fin.Induction` that allows one to avoid | ||
| the complicated use of `Acc`/`inject`/`raise` when proving inductive properties | ||
| over finite sets. | ||
|
|
||
| Bug-fixes | ||
| --------- | ||
|
|
||
| * Added missing module `Function.Metric` which re-exports | ||
| `Function.Metric.(Core/Definitions/Structures/Bundles)`. This module was referred | ||
| to in the documentation of its children but until now was not present. | ||
|
|
||
| * Added missing fixity declaration to `_<_` in | ||
| `Relation.Binary.Construct.NonStrictToStrict`. | ||
|
|
||
| Non-backwards compatible changes | ||
| -------------------------------- | ||
|
|
||
| #### Floating-point arithmetic | ||
|
|
||
| * The functions in `Data.Float.Base` were updated following changes upstream, | ||
| in `Agda.Builtin.Float`, see <https://github.com/agda/agda/pull/4885>. | ||
|
|
||
| * The bitwise binary relations on floating-point numbers (`_<_`, `_≈ᵇ_`, `_==_`) | ||
| have been removed without replacement, as they were deeply unintuitive, | ||
| e.g., `∀ x → x < -x`. | ||
|
|
||
| #### Reflection | ||
|
|
||
| * The representation of reflected syntax in `Reflection.Term`, | ||
| `Reflection.Pattern`, `Reflection.Argument` and | ||
| `Reflection.Argument.Information` has been updated to match the new | ||
| representation used in Agda 2.6.2. Specifically, the following | ||
| changes were made: | ||
|
|
||
| * The type of the `var` constructor of the `Pattern` datatype has | ||
| been changed from `(x : String) → Pattern` to `(x : Int) → | ||
| Pattern`. | ||
|
|
||
| * The type of the `dot` constructor of the `Pattern` datatype has | ||
| been changed from `Pattern` to `(t : Term) → Pattern`. | ||
|
|
||
| * The types of the `clause` and `absurd-clause` constructors of the | ||
| `Clause` datatype now take an extra argument `(tel : Telescope)`, | ||
| where `Telescope = List (String × Arg Type)`. | ||
|
|
||
| * The following constructors have been added to the `Sort` datatype: | ||
| `prop : (t : Term) → Sort`, `propLit : (n : Nat) → Sort`, and | ||
| `inf : (n : Nat) → Sort`. | ||
|
|
||
| * In `Reflection.Argument.Information` the function `relevance` was | ||
| replaced by `modality`. | ||
|
|
||
| * The type of the `arg-info` constructor is now | ||
| `(v : Visibility) (m : Modality) → ArgInfo`. | ||
|
|
||
| * In `Reflection.Argument` (as well as `Reflection`) there is a new | ||
| pattern synonym `defaultModality`, and the pattern synonyms | ||
| `vArg`, `hArg` and `iArg` have been changed. | ||
|
|
||
| * Two new modules have been added, `Reflection.Argument.Modality` | ||
| and `Reflection.Argument.Quantity`. The constructors of the types | ||
| `Modality` and `Quantity` are reexported from `Reflection`. | ||
|
|
||
| #### Sized types | ||
|
|
||
| * Sized types are no longer considered safe in Agda 2.6.2. As a | ||
| result, all modules that use `--sized-types` no longer have the | ||
| `--safe` flag. For a full list of affected modules, refer to the | ||
| relevant [commit](https://github.com/agda/agda-stdlib/pull/1465/files#diff-e1c0e3196e4cea6ff808f5d2906031a7657130e10181516206647b83c7014584R91-R131.) | ||
|
|
||
| * In order to maintain the safety of `Data.Nat.Pseudorandom.LCG`, the function | ||
| `stream` that relies on the newly unsafe `Codata` modules has | ||
| been moved to the new module `Data.Nat.Pseudorandom.LCG.Unsafe`. | ||
|
|
||
| * In order to maintain the safety of the modules in the `Codata.Musical` directory, | ||
| the functions `fromMusical` and `toMusical` defined in: | ||
| ``` | ||
| Codata.Musical.Colist | ||
| Codata.Musical.Conat | ||
| Codata.Musical.Cofin | ||
| Codata.Musical.M | ||
| Codata.Musical.Stream | ||
| ``` | ||
| have been moved to a new module `Codata.Musical.Conversion` and renamed to | ||
| `X.fromMusical` and `X.toMusical` for each of `Codata.Musical.X`. | ||
|
|
||
| * In order to maintain the safety of `Data.Container(.Indexed)`, the greatest fixpoint | ||
| of containers, `ν`, has been moved from `Data.Container(.Indexed)` to a new module | ||
| `Data.Container(.Indexed).Fixpoints.Guarded` which also re-exports the least fixpoint. | ||
|
|
||
| #### Other | ||
|
|
||
| * Replaced existing O(n) implementation of `Data.Nat.Binary.fromℕ` with a new O(log n) | ||
| implementation. The old implementation is maintained under `Data.Nat.Binary.fromℕ'` | ||
| and proven to be equivalent to the new one. | ||
|
|
||
| * `Data.Maybe.Base` now re-exports the definition of `Maybe` given by | ||
| `Agda.Builtin.Maybe`. The `Foreign.Haskell` modules and definitions | ||
| corresponding to `Maybe` have been removed. See the release notes of | ||
| Agda 2.6.2 for more information. | ||
|
|
||
| Deprecated modules | ||
| ------------------ | ||
|
|
||
| Deprecated names | ||
| ---------------- | ||
|
|
||
| New modules | ||
| ----------- | ||
|
|
||
| * New module for making system calls during type checking: | ||
| ```agda | ||
| Reflection.External | ||
| ``` | ||
|
|
||
| * New modules for universes and annotations of reflected syntax: | ||
| ``` | ||
| Reflection.Universe | ||
| Reflection.Annotated | ||
| Reflection.Annotated.Free | ||
| ``` | ||
|
|
||
| * Added new module for unary relations over sized types now that `Size` | ||
| lives in it's own universe since Agda 2.6.2. | ||
| ```agda | ||
| Relation.Unary.Sized | ||
| ``` | ||
|
|
||
| * Metrics specialised to co-domains with rational numbers: | ||
| ``` | ||
| Function.Metric.Rational | ||
| Function.Metric.Rational.Definitions | ||
| Function.Metric.Rational.Structures | ||
| Function.Metric.Rational.Bundles | ||
| ``` | ||
|
|
||
| * Lists that contain every element of a type: | ||
| ``` | ||
| Data.List.Relation.Unary.Enumerates.Setoid | ||
| Data.List.Relation.Unary.Enumerates.Setoid.Properties | ||
| ``` | ||
|
|
||
| * (Unsafe) sized W type: | ||
| ``` | ||
| Data.W.Sized | ||
| ``` | ||
|
|
||
| * (Unsafe) container fixpoints: | ||
| ``` | ||
| Data.Container.Fixpoints.Sized | ||
| ``` | ||
|
|
||
| Other minor additions | ||
| --------------------- | ||
|
|
||
| * Added new relations to `Data.Fin.Base`: | ||
| ```agda | ||
| _≥_ = ℕ._≥_ on toℕ | ||
| _>_ = ℕ._>_ on toℕ | ||
| ``` | ||
|
|
||
| * Added new proofs to `Data.Fin.Induction`: | ||
| ```agda | ||
| >-wellFounded : WellFounded {A = Fin n} _>_ | ||
| <-weakInduction : P zero → (∀ i → P (inject₁ i) → P (suc i)) → ∀ i → P i | ||
| >-weakInduction : P (fromℕ n) → (∀ i → P (suc i) → P (inject₁ i)) → ∀ i → P i | ||
| ``` | ||
|
|
||
| * Added new proofs to `Relation.Binary.Properties.Setoid`: | ||
| ```agda | ||
| respʳ-flip : _≈_ Respectsʳ (flip _≈_) | ||
| respˡ-flip : _≈_ Respectsˡ (flip _≈_) | ||
| ``` | ||
|
|
||
| * Added new function to `Data.Fin.Base`: | ||
| ```agda | ||
| pinch : Fin n → Fin (suc n) → Fin n | ||
| ``` | ||
|
|
||
| * Added new proofs to `Data.Fin.Properties`: | ||
| ```agda | ||
| pinch-surjective : Surjective _≡_ (pinch i) | ||
| pinch-mono-≤ : (pinch i) Preserves _≤_ ⟶ _≤_ | ||
| ``` | ||
|
|
||
| * Added new proofs to `Data.Nat.Binary.Properties`: | ||
| ```agda | ||
| fromℕ≡fromℕ' : fromℕ ≗ fromℕ' | ||
| toℕ-fromℕ' : toℕ ∘ fromℕ' ≗ id | ||
| fromℕ'-homo-+ : fromℕ' (m ℕ.+ n) ≡ fromℕ' m + fromℕ' n | ||
| ``` | ||
|
|
||
| * Rewrote proofs in `Data.Nat.Binary.Properties` for new implementation of `fromℕ`: | ||
| ```agda | ||
| toℕ-fromℕ : toℕ ∘ fromℕ ≗ id | ||
| fromℕ-homo-+ : fromℕ (m ℕ.+ n) ≡ fromℕ m + fromℕ n | ||
| ``` | ||
|
|
||
| * Added new proof to `Data.Nat.DivMod`: | ||
| ```agda | ||
| m/n≤m : (m / n) {≢0} ≤ m | ||
| ``` | ||
|
|
||
| * Added new type in `Size`: | ||
| ```agda | ||
| SizedSet ℓ = Size → Set ℓ | ||
| ``` | ||
| * The only change over v1.7 is that the library's Cabal file is now compatible with GHC 9.2. |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -1,2 +1,2 @@ | ||
| name: standard-library-1.7 | ||
| name: standard-library-1.7.1 | ||
| include: src |