diff --git a/src/Codata/Sized/Colist/Properties.agda b/src/Codata/Sized/Colist/Properties.agda index 76908cad6c..806a330ba2 100644 --- a/src/Codata/Sized/Colist/Properties.agda +++ b/src/Codata/Sized/Colist/Properties.agda @@ -144,10 +144,10 @@ module _ (cons : C → B → C) (alg : A → Maybe (A × B)) where scanl-unfold : ∀ nil a → i ⊢ scanl cons nil (unfold alg a) ≈ nil ∷ (λ where .force → unfold alg′ (a , nil)) - scanl-unfold nil a with alg a | Eq.inspect alg a - ... | nothing | [ eq ] = Eq.refl ∷ λ { .force → + scanl-unfold nil a with alg a in eq + ... | nothing = Eq.refl ∷ λ { .force → sym (fromEq (unfold-nothing (Maybeₚ.map-nothing eq))) } - ... | just (a′ , b) | [ eq ] = Eq.refl ∷ λ { .force → begin + ... | just (a′ , b) = Eq.refl ∷ λ { .force → begin scanl cons (cons nil b) (unfold alg a′) ≈⟨ scanl-unfold (cons nil b) a′ ⟩ (cons nil b ∷ _) diff --git a/src/Data/Fin/Properties.agda b/src/Data/Fin/Properties.agda index dd531dfe88..4fb32abbb7 100644 --- a/src/Data/Fin/Properties.agda +++ b/src/Data/Fin/Properties.agda @@ -587,13 +587,13 @@ remQuot-combine {suc n} {k} (suc i) j rewrite splitAt-↑ʳ k (n ℕ.* k) (com cong (Data.Product.map₁ suc) (remQuot-combine i j) combine-remQuot : ∀ {n} k (i : Fin (n ℕ.* k)) → uncurry combine (remQuot {n} k i) ≡ i -combine-remQuot {suc n} k i with splitAt k i | P.inspect (splitAt k) i -... | inj₁ j | P.[ eq ] = begin +combine-remQuot {suc n} k i with splitAt k i in eq +... | inj₁ j = begin join k (n ℕ.* k) (inj₁ j) ≡˘⟨ cong (join k (n ℕ.* k)) eq ⟩ join k (n ℕ.* k) (splitAt k i) ≡⟨ join-splitAt k (n ℕ.* k) i ⟩ i ∎ where open ≡-Reasoning -... | inj₂ j | P.[ eq ] = begin +... | inj₂ j = begin k ↑ʳ (uncurry combine (remQuot {n} k j)) ≡⟨ cong (k ↑ʳ_) (combine-remQuot {n} k j) ⟩ join k (n ℕ.* k) (inj₂ j) ≡˘⟨ cong (join k (n ℕ.* k)) eq ⟩ join k (n ℕ.* k) (splitAt k i) ≡⟨ join-splitAt k (n ℕ.* k) i ⟩ diff --git a/src/Data/List/Properties.agda b/src/Data/List/Properties.agda index 92976504aa..0714786c92 100644 --- a/src/Data/List/Properties.agda +++ b/src/Data/List/Properties.agda @@ -775,9 +775,9 @@ module _ {P : Pred A p} (P? : Decidable P) where filter-idem : filter P? ∘ filter P? ≗ filter P? filter-idem [] = refl - filter-idem (x ∷ xs) with does (P? x) | inspect does (P? x) - ... | false | _ = filter-idem xs - ... | true | P.[ eq ] rewrite eq = cong (x ∷_) (filter-idem xs) + filter-idem (x ∷ xs) with does (P? x) in eq + ... | false = filter-idem xs + ... | true rewrite eq = cong (x ∷_) (filter-idem xs) filter-++ : ∀ xs ys → filter P? (xs ++ ys) ≡ filter P? xs ++ filter P? ys filter-++ [] ys = refl diff --git a/src/Data/List/Relation/Binary/Permutation/Propositional/Properties.agda b/src/Data/List/Relation/Binary/Permutation/Propositional/Properties.agda index 2d60561d3c..43c1e4d7aa 100644 --- a/src/Data/List/Relation/Binary/Permutation/Propositional/Properties.agda +++ b/src/Data/List/Relation/Binary/Permutation/Propositional/Properties.agda @@ -29,7 +29,7 @@ open import Level using (Level) open import Relation.Unary using (Pred) open import Relation.Binary open import Relation.Binary.PropositionalEquality as ≡ - using (_≡_ ; refl ; cong; cong₂; _≢_; inspect) + using (_≡_ ; refl ; cong; cong₂; _≢_) open import Relation.Nullary open PermutationReasoning diff --git a/src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda b/src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda index 2bcfbf094e..37af9a67a8 100644 --- a/src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda +++ b/src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda @@ -38,7 +38,7 @@ open import Level using (Level; _⊔_) open import Relation.Unary using (Pred; Decidable) open import Relation.Binary.Properties.Setoid S using (≉-resp₂) open import Relation.Binary.PropositionalEquality as ≡ - using (_≡_ ; refl; sym; cong; cong₂; subst; _≢_; inspect) + using (_≡_ ; refl; sym; cong; cong₂; subst; _≢_) open import Relation.Nullary using (yes; no; does) open import Relation.Nullary.Negation using (contradiction) diff --git a/src/Data/List/Relation/Unary/Any/Properties.agda b/src/Data/List/Relation/Unary/Any/Properties.agda index 243c97e0eb..aa40e987ff 100644 --- a/src/Data/List/Relation/Unary/Any/Properties.agda +++ b/src/Data/List/Relation/Unary/Any/Properties.agda @@ -42,7 +42,7 @@ open import Function.Related as Related using (Kind; Related; SK-sym) open import Level using (Level) open import Relation.Binary as B hiding (_⇔_) open import Relation.Binary.PropositionalEquality as P - using (_≡_; refl; inspect) + using (_≡_; refl) open import Relation.Unary as U using (Pred; _⟨×⟩_; _⟨→⟩_) renaming (_⊆_ to _⋐_) open import Relation.Nullary using (¬_; _because_; does; ofʸ; ofⁿ; yes; no) @@ -171,9 +171,9 @@ any⁺ p (there {x = x} pxs) with p x ... | false = any⁺ p pxs any⁻ : ∀ (p : A → Bool) xs → T (any p xs) → Any (T ∘ p) xs -any⁻ p (x ∷ xs) px∷xs with p x | inspect p x -... | true | P.[ eq ] = here (Equivalence.from T-≡ ⟨$⟩ eq) -... | false | _ = there (any⁻ p xs px∷xs) +any⁻ p (x ∷ xs) px∷xs with p x in eq +... | true = here (Equivalence.from T-≡ ⟨$⟩ eq) +... | false = there (any⁻ p xs px∷xs) any⇔ : ∀ {p : A → Bool} → Any (T ∘ p) xs ⇔ T (any p xs) any⇔ = equivalence (any⁺ _) (any⁻ _ _) diff --git a/src/Data/Rational/Properties.agda b/src/Data/Rational/Properties.agda index 125230f45e..a1b26f203a 100644 --- a/src/Data/Rational/Properties.agda +++ b/src/Data/Rational/Properties.agda @@ -1337,24 +1337,24 @@ neg-distribʳ-* = +-*-Monomorphism.neg-distribʳ-* ℚᵘ.+-0-isGroup ℚᵘ.*-i ------------------------------------------------------------------------ p≤q⇒p⊔q≡q : p ≤ q → p ⊔ q ≡ q -p≤q⇒p⊔q≡q {p} {q} p≤q with p ≤ᵇ q | inspect (p ≤ᵇ_) q -... | true | _ = refl -... | false | [ p≰q ] = contradiction (≤⇒≤ᵇ p≤q) (subst (¬_ ∘ T) (sym p≰q) λ()) +p≤q⇒p⊔q≡q {p} {q} p≤q with p ≤ᵇ q in eq +... | true = refl +... | false = contradiction (≤⇒≤ᵇ p≤q) (subst (¬_ ∘ T) (sym eq) λ()) p≥q⇒p⊔q≡p : p ≥ q → p ⊔ q ≡ p -p≥q⇒p⊔q≡p {p} {q} p≥q with p ≤ᵇ q | inspect (p ≤ᵇ_) q -... | true | [ p≤q ] = ≤-antisym p≥q (≤ᵇ⇒≤ (subst T (sym p≤q) _)) -... | false | [ p≤q ] = refl +p≥q⇒p⊔q≡p {p} {q} p≥q with p ≤ᵇ q in eq +... | true = ≤-antisym p≥q (≤ᵇ⇒≤ (subst T (sym eq) _)) +... | false = refl p≤q⇒p⊓q≡p : p ≤ q → p ⊓ q ≡ p -p≤q⇒p⊓q≡p {p} {q} p≤q with p ≤ᵇ q | inspect (p ≤ᵇ_) q -... | true | _ = refl -... | false | [ p≰q ] = contradiction (≤⇒≤ᵇ p≤q) (subst (¬_ ∘ T) (sym p≰q) λ()) +p≤q⇒p⊓q≡p {p} {q} p≤q with p ≤ᵇ q in eq +... | true = refl +... | false = contradiction (≤⇒≤ᵇ p≤q) (subst (¬_ ∘ T) (sym eq) λ()) p≥q⇒p⊓q≡q : p ≥ q → p ⊓ q ≡ q -p≥q⇒p⊓q≡q {p} {q} p≥q with p ≤ᵇ q | inspect (p ≤ᵇ_) q -... | true | [ p≤q ] = ≤-antisym (≤ᵇ⇒≤ (subst T (sym p≤q) _)) p≥q -... | false | [ p≤q ] = refl +p≥q⇒p⊓q≡q {p} {q} p≥q with p ≤ᵇ q in eq +... | true = ≤-antisym (≤ᵇ⇒≤ (subst T (sym eq) _)) p≥q +... | false = refl ⊓-operator : MinOperator ≤-totalPreorder ⊓-operator = record diff --git a/src/Data/Rational/Unnormalised/Properties.agda b/src/Data/Rational/Unnormalised/Properties.agda index 619218afc3..4221eef658 100644 --- a/src/Data/Rational/Unnormalised/Properties.agda +++ b/src/Data/Rational/Unnormalised/Properties.agda @@ -1446,24 +1446,24 @@ p>1⇒1/p<1 {p} p>1 = lemma′ p (p>1⇒p≢0 p>1) p>1 -- Basic specification in terms of _≤_ p≤q⇒p⊔q≃q : p ≤ q → p ⊔ q ≃ q -p≤q⇒p⊔q≃q {p} {q} p≤q with p ≤ᵇ q | inspect (p ≤ᵇ_) q -... | true | _ = ≃-refl -... | false | [ p≰q ] = contradiction (≤⇒≤ᵇ p≤q) (subst (¬_ ∘ T) (sym p≰q) λ()) +p≤q⇒p⊔q≃q {p} {q} p≤q with p ≤ᵇ q in eq +... | true = ≃-refl +... | false = contradiction (≤⇒≤ᵇ p≤q) (subst (¬_ ∘ T) (sym eq) λ()) p≥q⇒p⊔q≃p : p ≥ q → p ⊔ q ≃ p -p≥q⇒p⊔q≃p {p} {q} p≥q with p ≤ᵇ q | inspect (p ≤ᵇ_) q -... | true | [ p≤q ] = ≤-antisym p≥q (≤ᵇ⇒≤ (subst T (sym p≤q) _)) -... | false | [ p≤q ] = ≃-refl +p≥q⇒p⊔q≃p {p} {q} p≥q with p ≤ᵇ q in eq +... | true = ≤-antisym p≥q (≤ᵇ⇒≤ (subst T (sym eq) _)) +... | false = ≃-refl p≤q⇒p⊓q≃p : p ≤ q → p ⊓ q ≃ p -p≤q⇒p⊓q≃p {p} {q} p≤q with p ≤ᵇ q | inspect (p ≤ᵇ_) q -... | true | _ = ≃-refl -... | false | [ p≰q ] = contradiction (≤⇒≤ᵇ p≤q) (subst (¬_ ∘ T) (sym p≰q) λ()) +p≤q⇒p⊓q≃p {p} {q} p≤q with p ≤ᵇ q in eq +... | true = ≃-refl +... | false = contradiction (≤⇒≤ᵇ p≤q) (subst (¬_ ∘ T) (sym eq) λ()) p≥q⇒p⊓q≃q : p ≥ q → p ⊓ q ≃ q -p≥q⇒p⊓q≃q {p} {q} p≥q with p ≤ᵇ q | inspect (p ≤ᵇ_) q -... | true | [ p≤q ] = ≤-antisym (≤ᵇ⇒≤ (subst T (sym p≤q) _)) p≥q -... | false | [ p≤q ] = ≃-refl +p≥q⇒p⊓q≃q {p} {q} p≥q with p ≤ᵇ q in eq +... | true = ≤-antisym (≤ᵇ⇒≤ (subst T (sym eq) _)) p≥q +... | false = ≃-refl ⊓-operator : MinOperator ≤-totalPreorder ⊓-operator = record diff --git a/src/Data/Vec/Relation/Unary/Any/Properties.agda b/src/Data/Vec/Relation/Unary/Any/Properties.agda index a300c44d55..bd4e6053d7 100644 --- a/src/Data/Vec/Relation/Unary/Any/Properties.agda +++ b/src/Data/Vec/Relation/Unary/Any/Properties.agda @@ -333,13 +333,11 @@ module _ {P : Pred A p} where concat⁺∘concat⁻ : ∀ {n m} (xss : Vec (Vec A n) m) (p : Any P (concat xss)) → concat⁺ (concat⁻ xss p) ≡ p - concat⁺∘concat⁻ (xs ∷ xss) p with ++⁻ xs p | P.inspect (++⁻ xs) p - ... | inj₁ pxs | P.[ p=inj₁ ] - = P.trans (P.cong [ ++⁺ˡ , ++⁺ʳ xs ]′ (P.sym p=inj₁)) - $ ++⁺∘++⁻ xs p - ... | inj₂ pxss | P.[ p=inj₂ ] rewrite concat⁺∘concat⁻ xss pxss - = P.trans (P.cong [ ++⁺ˡ , ++⁺ʳ xs ]′ (P.sym p=inj₂)) - $ ++⁺∘++⁻ xs p + concat⁺∘concat⁻ (xs ∷ xss) p with ++⁻ xs p in eq + ... | inj₁ pxs + = P.trans (P.cong [ ++⁺ˡ , ++⁺ʳ xs ]′ (P.sym eq)) $ ++⁺∘++⁻ xs p + ... | inj₂ pxss rewrite concat⁺∘concat⁻ xss pxss + = P.trans (P.cong [ ++⁺ˡ , ++⁺ʳ xs ]′ (P.sym eq)) $ ++⁺∘++⁻ xs p concat⁻∘concat⁺ : ∀ {n m} {xss : Vec (Vec A n) m} (p : Any (Any P) xss) → concat⁻ xss (concat⁺ p) ≡ p diff --git a/src/Relation/Binary/PropositionalEquality.agda b/src/Relation/Binary/PropositionalEquality.agda index 72a311bd8b..877204ed38 100644 --- a/src/Relation/Binary/PropositionalEquality.agda +++ b/src/Relation/Binary/PropositionalEquality.agda @@ -60,24 +60,6 @@ _≗_ {A = A} {B = B} = Setoid._≈_ (A →-setoid B) (A → Setoid.Carrier B) → setoid A ⟶ B →-to-⟶ = :→-to-Π ------------------------------------------------------------------------- --- Inspect - --- Inspect can be used when you want to pattern match on the result r --- of some expression e, and you also need to "remember" that r ≡ e. - --- See README.Inspect for an explanation of how/why to use this. - -record Reveal_·_is_ {A : Set a} {B : A → Set b} - (f : (x : A) → B x) (x : A) (y : B x) : - Set (a ⊔ b) where - constructor [_] - field eq : f x ≡ y - -inspect : ∀ {A : Set a} {B : A → Set b} - (f : (x : A) → B x) (x : A) → Reveal f · x is f x -inspect f x = [ refl ] - ------------------------------------------------------------------------ -- Propositionality @@ -120,3 +102,31 @@ module _ (_≟_ : Decidable {A = A} _≡_) {x y : A} where ≢-≟-identity : x ≢ y → ∃ λ ¬eq → x ≟ y ≡ no ¬eq ≢-≟-identity ¬eq = dec-no (x ≟ y) ¬eq + + +------------------------------------------------------------------------ +-- DEPRECATED NAMES +------------------------------------------------------------------------ +-- Please use the new names as continuing support for the old names is +-- not guaranteed. + +-- Version 2.0 + +record Reveal_·_is_ {A : Set a} {B : A → Set b} + (f : (x : A) → B x) (x : A) (y : B x) : + Set (a ⊔ b) where + constructor [_] + field eq : f x ≡ y + +inspect : ∀ {A : Set a} {B : A → Set b} + (f : (x : A) → B x) (x : A) → Reveal f · x is f x +inspect f x = [ refl ] + +{-# WARNING_ON_USAGE Reveal_·_is_ +"Warning: Reveal_·_is_ was deprecated in v2.0. +Please use new `with ... in` syntax described at https://agda.readthedocs.io/en/v2.6.2/language/with-abstraction.html#with-abstraction-equality instead." +#-} +{-# WARNING_ON_USAGE inspect +"Warning: inspect was deprecated in v2.0. +Please use new `with ... in` syntax described at https://agda.readthedocs.io/en/v2.6.2/language/with-abstraction.html#with-abstraction-equality instead." +#-}