diff --git a/CHANGELOG.md b/CHANGELOG.md index 5891740538..1da4157a62 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -371,42 +371,42 @@ Non-backwards compatible changes `m / n` without having to explicitly provide a proof, as instance search will fill it in for you. The full list of such operations changed is as follows: - In `Data.Nat.DivMod`: `_/_`, `_%_`, `_div_`, `_mod_` - - In `Data.Nat.Pseudorandom.LCG`: `Generator` - - In `Data.Integer.DivMod`: `_divℕ_`, `_div_`, `_modℕ_`, `_mod_` - - In `Data.Rational`: `mkℚ+`, `normalize`, `_/_`, `1/_` - - In `Data.Rational.Unnormalised`: `_/_`, `1/_`, `_÷_` + - In `Data.Nat.Pseudorandom.LCG`: `Generator` + - In `Data.Integer.DivMod`: `_divℕ_`, `_div_`, `_modℕ_`, `_mod_` + - In `Data.Rational`: `mkℚ+`, `normalize`, `_/_`, `1/_` + - In `Data.Rational.Unnormalised`: `_/_`, `1/_`, `_÷_` * At the moment, there are 4 different ways such instance arguments can be provided, listed in order of convenience and clarity: 1. *Automatic basic instances* - the standard library provides instances based on the constructors of each - numeric type in `Data.X.Base`. For example, `Data.Nat.Base` constains an instance of `NonZero (suc n)` for any `n` - and `Data.Integer.Base` contains an instance of `NonNegative (+ n)` for any `n`. Consequently, - if the argument is of the required form, these instances will always be filled in by instance search - automatically, e.g. - ``` - 0/n≡0 : 0 / suc n ≡ 0 - ``` - 2. *Take the instance as an argument* - You can provide the instance argument as a parameter to your function - and Agda's instance search will automatically use it in the correct place without you having to - explicitly pass it, e.g. - ``` - 0/n≡0 : .{{_ : NonZero n}} → 0 / n ≡ 0 - ``` - 3. *Define the instance locally* - You can define an instance argument in scope (e.g. in a `where` clause) - and Agda's instance search will again find it automatically, e.g. - ``` - instance - n≢0 : NonZero n - n≢0 = ... - - 0/n≡0 : 0 / n ≡ 0 - ``` - 4. *Pass the instance argument explicitly* - Finally, if all else fails you can pass the - instance argument explicitly into the function using `{{ }}`, e.g. - ``` - 0/n≡0 : ∀ n (n≢0 : NonZero n) → ((0 / n) {{n≢0}}) ≡ 0 - ``` - Suitable constructors for `NonZero`/`Positive` etc. can be found in `Data.X.Base`. + numeric type in `Data.X.Base`. For example, `Data.Nat.Base` constains an instance of `NonZero (suc n)` for any `n` + and `Data.Integer.Base` contains an instance of `NonNegative (+ n)` for any `n`. Consequently, + if the argument is of the required form, these instances will always be filled in by instance search + automatically, e.g. + ``` + 0/n≡0 : 0 / suc n ≡ 0 + ``` + 2. *Take the instance as an argument* - You can provide the instance argument as a parameter to your function + and Agda's instance search will automatically use it in the correct place without you having to + explicitly pass it, e.g. + ``` + 0/n≡0 : .{{_ : NonZero n}} → 0 / n ≡ 0 + ``` + 3. *Define the instance locally* - You can define an instance argument in scope (e.g. in a `where` clause) + and Agda's instance search will again find it automatically, e.g. + ``` + instance + n≢0 : NonZero n + n≢0 = ... + + 0/n≡0 : 0 / n ≡ 0 + ``` + 4. *Pass the instance argument explicitly* - Finally, if all else fails you can pass the + instance argument explicitly into the function using `{{ }}`, e.g. + ``` + 0/n≡0 : ∀ n (n≢0 : NonZero n) → ((0 / n) {{n≢0}}) ≡ 0 + ``` + Suitable constructors for `NonZero`/`Positive` etc. can be found in `Data.X.Base`. * A full list of proofs that have changed to use instance arguments is available at the end of this file. Notable changes to proofs are now discussed below. @@ -457,14 +457,14 @@ Non-backwards compatible changes * As a consequence of this, some proofs that relied on this reduction behaviour or on eta-equality may no longer go through. There are several ways to fix this: 1. The principled way is to not rely on this reduction behaviour in the first place. - The `Properties` files for rational numbers have been greatly expanded in `v1.7` - and `v2.0`, and we believe most proofs should be able to be built up from existing - proofs contained within these files. + The `Properties` files for rational numbers have been greatly expanded in `v1.7` + and `v2.0`, and we believe most proofs should be able to be built up from existing + proofs contained within these files. 2. Alternatively, annotating any rational arguments to a proof with either - `@record{}` or `@(mkℚ _ _ _)` should restore the old reduction behaviour for any - terms involving those parameters. + `@record{}` or `@(mkℚ _ _ _)` should restore the old reduction behaviour for any + terms involving those parameters. 3. Finally, if the above approaches are not viable then you may be forced to explicitly - use `cong` combined with a lemma that proves the old reduction behaviour. + use `cong` combined with a lemma that proves the old reduction behaviour. ### Change to the definition of `LeftCancellative` and `RightCancellative` @@ -478,20 +478,20 @@ Non-backwards compatible changes * Therefore the definitions have been changed as follows to make all their arguments explicit: - `LeftCancellative _•_` - - From: `∀ x {y z} → (x • y) ≈ (x • z) → y ≈ z` - - To: `∀ x y z → (x • y) ≈ (x • z) → y ≈ z` + - From: `∀ x {y z} → (x • y) ≈ (x • z) → y ≈ z` + - To: `∀ x y z → (x • y) ≈ (x • z) → y ≈ z` - `RightCancellative _•_` - From: `∀ {x} y z → (y • x) ≈ (z • x) → y ≈ z` - - To: `∀ x y z → (y • x) ≈ (z • x) → y ≈ z` + - To: `∀ x y z → (y • x) ≈ (z • x) → y ≈ z` - `AlmostLeftCancellative e _•_` - From: `∀ {x} y z → ¬ x ≈ e → (x • y) ≈ (x • z) → y ≈ z` - - To: `∀ x y z → ¬ x ≈ e → (x • y) ≈ (x • z) → y ≈ z` + - To: `∀ x y z → ¬ x ≈ e → (x • y) ≈ (x • z) → y ≈ z` - `AlmostRightCancellative e _•_` - - From: `∀ {x} y z → ¬ x ≈ e → (y • x) ≈ (z • x) → y ≈ z` - - To: `∀ x y z → ¬ x ≈ e → (y • x) ≈ (z • x) → y ≈ z` + - From: `∀ {x} y z → ¬ x ≈ e → (y • x) ≈ (z • x) → y ≈ z` + - To: `∀ x y z → ¬ x ≈ e → (y • x) ≈ (z • x) → y ≈ z` * Correspondingly some proofs of the above types will need additional arguments passed explicitly. Instances can easily be fixed by adding additional underscores, e.g. @@ -643,7 +643,7 @@ Non-backwards compatible changes - `¬?` has been moved from `Relation.Nullary.Negation.Core` to `Relation.Nullary.Decidable.Core` - `¬-reflects` has been moved from `Relation.Nullary.Negation.Core` to `Relation.Nullary.Reflects`. - `decidable-stable`, `excluded-middle` and `¬-drop-Dec` have been moved from `Relation.Nullary.Negation` - to `Relation.Nullary.Decidable`. + to `Relation.Nullary.Decidable`. - `fromDec` and `toDec` have been mvoed from `Data.Sum.Base` to `Data.Sum`. ### Refactoring of the unindexed Functor/Applicative/Monad hiearchy @@ -733,6 +733,13 @@ Non-backwards compatible changes * In accordance with changes to the flags in Agda 2.6.3, all modules that previously used the `--without-K` flag now use the `--cubical-compatible` flag instead. +* To avoid _large indices_ that are by default no longer allowed in Agda 2.6.4, + universe levels have been increased in the following definitions: + - `Data.Star.Decoration.DecoratedWith` + - `Data.Star.Pointer.Pointer` + - `Reflection.AnnotatedAST.Typeₐ` + - `Reflection.AnnotatedAST.AnnotationFun` + * The first two arguments of `m≡n⇒m-n≡0` (now `i≡j⇒i-j≡0`) in `Data.Integer.Base` have been made implicit. @@ -883,13 +890,13 @@ Major improvements * The ring solver tactic has been greatly improved. In particular: 1. When the solver is used for concrete ring types, e.g. ℤ, the equality can now use - all the ring operations defined natively for that type, rather than having - to use the operations defined in `AlmostCommutativeRing`. For example - previously you could not use `Data.Integer.Base._*_` but instead had to - use `AlmostCommutativeRing._*_`. + all the ring operations defined natively for that type, rather than having + to use the operations defined in `AlmostCommutativeRing`. For example + previously you could not use `Data.Integer.Base._*_` but instead had to + use `AlmostCommutativeRing._*_`. 2. The solver now supports use of the subtraction operator `_-_` whenever it is defined immediately in terms of `_+_` and `-_`. This is the case for - `Data.Integer` and `Data.Rational`. + `Data.Integer` and `Data.Rational`. ### Moved `_%_` and `_/_` operators to `Data.Nat.Base` @@ -2165,9 +2172,9 @@ Other minor changes take-suc-tabulate : (f : Fin n → A) (o : Fin n) → let m = toℕ o in take (suc m) (tabulate f) ≡ take m (tabulate f) ∷ʳ f o drop-take-suc : (o : Fin (length xs)) → let m = toℕ o in drop m (take (suc m) xs) ≡ [ lookup xs o ] drop-take-suc-tabulate : (f : Fin n → A) (o : Fin n) → let m = toℕ o in drop m (take (suc m) (tabulate f)) ≡ [ f o ] - - take-all : n ≥ length xs → take n xs ≡ xs - + + take-all : n ≥ length xs → take n xs ≡ xs + take-[] : ∀ m → take m [] ≡ [] drop-[] : ∀ m → drop m [] ≡ [] ``` @@ -2901,7 +2908,7 @@ Other minor changes foldr-map : foldr f x (map g xs) ≡ foldr (g -⟨ f ∣) x xs foldl-map : foldl f x (map g xs) ≡ foldl (∣ f ⟩- g) x xs ``` - + NonZero/Positive/Negative changes --------------------------------- diff --git a/src/Data/Star/Decoration.agda b/src/Data/Star/Decoration.agda index 24428a5843..170b5abb07 100644 --- a/src/Data/Star/Decoration.agda +++ b/src/Data/Star/Decoration.agda @@ -28,7 +28,7 @@ data NonEmptyEdgePred {ℓ r p : Level} {I : Set ℓ} (T : Rel I r) -- Decorating an edge with more information. data DecoratedWith {ℓ r p : Level} {I : Set ℓ} {T : Rel I r} (P : EdgePred p T) - : Rel (NonEmpty (Star T)) p where + : Rel (NonEmpty (Star T)) (ℓ ⊔ r ⊔ p) where ↦ : ∀ {i j k} {x : T i j} {xs : Star T j k} (p : P x) → DecoratedWith P (nonEmpty (x ◅ xs)) (nonEmpty xs) diff --git a/src/Data/Star/Pointer.agda b/src/Data/Star/Pointer.agda index ed606807ce..bc86786f74 100644 --- a/src/Data/Star/Pointer.agda +++ b/src/Data/Star/Pointer.agda @@ -26,7 +26,7 @@ private data Pointer {T : Rel I r} (P : EdgePred p T) (Q : EdgePred q T) - : Rel (Maybe (NonEmpty (Star T))) (p ⊔ q) where + : Rel (Maybe (NonEmpty (Star T))) (ℓ ⊔ r ⊔ p ⊔ q) where step : ∀ {i j k} {x : T i j} {xs : Star T j k} (p : P x) → Pointer P Q (just (nonEmpty (x ◅ xs))) (just (nonEmpty xs)) diff --git a/src/Reflection/AnnotatedAST.agda b/src/Reflection/AnnotatedAST.agda index 61d55def7d..8ebc54b919 100644 --- a/src/Reflection/AnnotatedAST.agda +++ b/src/Reflection/AnnotatedAST.agda @@ -35,8 +35,8 @@ Annotation : ∀ ℓ → Set (suc ℓ) Annotation ℓ = ∀ {u} → ⟦ u ⟧ → Set ℓ -- An annotated type is a family over an Annotation and a reflected term. -Typeₐ : ∀ ℓ → Univ → Set (suc ℓ) -Typeₐ ℓ u = Annotation ℓ → ⟦ u ⟧ → Set ℓ +Typeₐ : ∀ ℓ → Univ → Set (suc (suc ℓ)) +Typeₐ ℓ u = Annotation ℓ → ⟦ u ⟧ → Set (suc ℓ) private variable @@ -168,7 +168,7 @@ mutual -- An annotation function computes the top-level annotation given a -- term annotated at all sub-terms. -AnnotationFun : Annotation ℓ → Set ℓ +AnnotationFun : Annotation ℓ → Set (suc ℓ) AnnotationFun Ann = ∀ u {t : ⟦ u ⟧} → Annotated′ Ann t → Ann t