diff --git a/src/Algebra/Construct/LexProduct.agda b/src/Algebra/Construct/LexProduct.agda index 65a6b80ba1..3fbcf86c80 100644 --- a/src/Algebra/Construct/LexProduct.agda +++ b/src/Algebra/Construct/LexProduct.agda @@ -11,7 +11,7 @@ open import Algebra.Definitions open import Data.Bool.Base using (true; false) open import Data.Product.Base using (_×_; _,_) open import Data.Product.Relation.Binary.Pointwise.NonDependent using (Pointwise) -open import Data.Sum.Base using (inj₁; inj₂) +open import Data.Sum.Base using (inj₁; inj₂; map) open import Function.Base using (_∘_) open import Relation.Binary.Core using (Rel) open import Relation.Binary.Definitions using (Decidable) @@ -107,6 +107,4 @@ sel ∙-sel ◦-sel (a , x) (b , y) with (a ∙ b) ≟₁ a | (a ∙ b) ≟₁ b ... | no ab≉a | no ab≉b = contradiction₂ (∙-sel a b) ab≉a ab≉b ... | yes ab≈a | no _ = inj₁ (ab≈a , ≈₂-refl) ... | no _ | yes ab≈b = inj₂ (ab≈b , ≈₂-refl) -... | yes ab≈a | yes ab≈b with ◦-sel x y -... | inj₁ xy≈x = inj₁ (ab≈a , xy≈x) -... | inj₂ xy≈y = inj₂ (ab≈b , xy≈y) +... | yes ab≈a | yes ab≈b = map (ab≈a ,_) (ab≈b ,_) (◦-sel x y) diff --git a/src/Algebra/Construct/LiftedChoice.agda b/src/Algebra/Construct/LiftedChoice.agda index 2377650cf8..e3d37009ed 100644 --- a/src/Algebra/Construct/LiftedChoice.agda +++ b/src/Algebra/Construct/LiftedChoice.agda @@ -11,13 +11,14 @@ open import Algebra module Algebra.Construct.LiftedChoice where open import Algebra.Consequences.Base -open import Relation.Binary.Core using (Rel; _⇒_; _Preserves_⟶_) -open import Relation.Binary.Structures using (IsEquivalence) -open import Relation.Nullary using (¬_; yes; no) -open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂; [_,_]) +open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂; [_,_]; [_,_]′) open import Data.Product.Base using (_×_; _,_) +open import Function.Base using (const; _$_) open import Level using (Level; _⊔_) +open import Relation.Binary.Core using (Rel; _⇒_; _Preserves_⟶_) +open import Relation.Nullary using (¬_; yes; no) open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_) +open import Relation.Binary.Structures using (IsEquivalence) open import Relation.Unary using (Pred) import Relation.Binary.Reasoning.Setoid as ≈-Reasoning @@ -34,9 +35,7 @@ private module _ (_≈_ : Rel B ℓ) (_•_ : Op₂ B) where Lift : Selective _≈_ _•_ → (A → B) → Op₂ A - Lift ∙-sel f x y with ∙-sel (f x) (f y) - ... | inj₁ _ = x - ... | inj₂ _ = y + Lift ∙-sel f x y = [ const x , const y ]′ $ ∙-sel (f x) (f y) ------------------------------------------------------------------------ -- Algebraic properties diff --git a/src/Algebra/Construct/NaturalChoice/MinOp.agda b/src/Algebra/Construct/NaturalChoice/MinOp.agda index 22d0686f8f..7ad8983a1f 100644 --- a/src/Algebra/Construct/NaturalChoice/MinOp.agda +++ b/src/Algebra/Construct/NaturalChoice/MinOp.agda @@ -39,13 +39,13 @@ open import Relation.Binary.Reasoning.Preorder preorder x⊓y≤x : ∀ x y → x ⊓ y ≤ x x⊓y≤x x y with total x y -... | inj₁ x≤y = ≤-respˡ-≈ (Eq.sym (x≤y⇒x⊓y≈x x≤y)) refl +... | inj₁ x≤y = reflexive (x≤y⇒x⊓y≈x x≤y) ... | inj₂ y≤x = ≤-respˡ-≈ (Eq.sym (x≥y⇒x⊓y≈y y≤x)) y≤x x⊓y≤y : ∀ x y → x ⊓ y ≤ y x⊓y≤y x y with total x y ... | inj₁ x≤y = ≤-respˡ-≈ (Eq.sym (x≤y⇒x⊓y≈x x≤y)) x≤y -... | inj₂ y≤x = ≤-respˡ-≈ (Eq.sym (x≥y⇒x⊓y≈y y≤x)) refl +... | inj₂ y≤x = reflexive (x≥y⇒x⊓y≈y y≤x) ------------------------------------------------------------------------ -- Algebraic properties diff --git a/src/Codata/Sized/Cowriter.agda b/src/Codata/Sized/Cowriter.agda index 03d24d3d3c..fd4ba91787 100644 --- a/src/Codata/Sized/Cowriter.agda +++ b/src/Codata/Sized/Cowriter.agda @@ -113,6 +113,7 @@ _>>=_ : ∀ {i} → Cowriter W A i → (A → Cowriter W X i) → Cowriter W X i -- Construction. unfold : ∀ {i} → (X → (W × X) ⊎ A) → X → Cowriter W A i -unfold next seed with next seed -... | inj₁ (w , seed′) = w ∷ λ where .force → unfold next seed′ -... | inj₂ a = [ a ] +unfold next seed = + Sum.[ (λ where (w , seed′) → w ∷ λ where .force → unfold next seed′) + , [_] + ] (next seed) diff --git a/src/Data/Fin/Base.agda b/src/Data/Fin/Base.agda index d762e10007..a328a85a57 100644 --- a/src/Data/Fin/Base.agda +++ b/src/Data/Fin/Base.agda @@ -15,7 +15,7 @@ open import Data.Bool.Base using (Bool; T) open import Data.Nat.Base as ℕ using (ℕ; zero; suc) open import Data.Product.Base as Product using (_×_; _,_; proj₁; proj₂) open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂; [_,_]′) -open import Function.Base using (id; _∘_; _on_; flip) +open import Function.Base using (id; _∘_; _on_; flip; _$_) open import Level using (0ℓ) open import Relation.Binary.Core open import Relation.Binary.PropositionalEquality.Core using (_≡_; _≢_; refl; cong) @@ -134,7 +134,7 @@ strengthen (suc i) = suc (strengthen i) splitAt : ∀ m {n} → Fin (m ℕ.+ n) → Fin m ⊎ Fin n splitAt zero i = inj₂ i splitAt (suc m) zero = inj₁ zero -splitAt (suc m) (suc i) = Sum.map suc id (splitAt m i) +splitAt (suc m) (suc i) = Sum.map₁ suc (splitAt m i) -- inverse of above function join : ∀ m n → Fin m ⊎ Fin n → Fin (m ℕ.+ n) @@ -144,9 +144,10 @@ join m n = [ _↑ˡ n , m ↑ʳ_ ]′ -- This is dual to group from Data.Vec. quotRem : ∀ n → Fin (m ℕ.* n) → Fin n × Fin m -quotRem {suc m} n i with splitAt n i -... | inj₁ j = j , zero -... | inj₂ j = Product.map₂ suc (quotRem {m} n j) +quotRem {suc m} n i = + [ (_, zero) + , Product.map₂ suc ∘ quotRem {m} n + ]′ $ splitAt n i -- a variant of quotRem the type of whose result matches the order of multiplication remQuot : ∀ n → Fin (m ℕ.* n) → Fin m × Fin n diff --git a/src/Data/List/Fresh.agda b/src/Data/List/Fresh.agda index 3375b0d54a..028e186567 100644 --- a/src/Data/List/Fresh.agda +++ b/src/Data/List/Fresh.agda @@ -14,7 +14,7 @@ module Data.List.Fresh where open import Level using (Level; _⊔_) -open import Data.Bool.Base using (true; false) +open import Data.Bool.Base using (true; false; if_then_else_) open import Data.Unit.Polymorphic.Base using (⊤) open import Data.Product.Base using (∃; _×_; _,_; -,_; proj₁; proj₂) open import Data.List.Relation.Unary.All using (All; []; _∷_) @@ -161,10 +161,10 @@ module _ {P : Pred A p} (P? : U.Decidable P) where takeWhile-# : ∀ {R : Rel A r} a (as : List# A R) → a # as → a # takeWhile as takeWhile [] = [] - takeWhile (cons a as ps) with does (P? a) - ... | true = cons a (takeWhile as) (takeWhile-# a as ps) - ... | false = [] + takeWhile (cons a as ps) = + if does (P? a) then cons a (takeWhile as) (takeWhile-# a as ps) else [] + -- this 'with' is needed to cause reduction in the type of 'takeWhile (a ∷# as)' takeWhile-# a [] _ = _ takeWhile-# a (x ∷# xs) (p , ps) with does (P? x) ... | true = p , takeWhile-# a xs ps @@ -172,18 +172,17 @@ module _ {P : Pred A p} (P? : U.Decidable P) where dropWhile : {R : Rel A r} → List# A R → List# A R dropWhile [] = [] - dropWhile aas@(a ∷# as) with does (P? a) - ... | true = dropWhile as - ... | false = aas + dropWhile aas@(a ∷# as) = if does (P? a) then dropWhile as else aas filter : {R : Rel A r} → List# A R → List# A R filter-# : ∀ {R : Rel A r} a (as : List# A R) → a # as → a # filter as filter [] = [] - filter (cons a as ps) with does (P? a) - ... | true = cons a (filter as) (filter-# a as ps) - ... | false = filter as + filter (cons a as ps) = + let l = filter as in + if does (P? a) then cons a l (filter-# a as ps) else l + -- this 'with' is needed to cause reduction in the type of 'filter-# a (x ∷# xs)' filter-# a [] _ = _ filter-# a (x ∷# xs) (p , ps) with does (P? x) ... | true = p , filter-# a xs ps diff --git a/src/Data/List/Fresh/Relation/Unary/All.agda b/src/Data/List/Fresh/Relation/Unary/All.agda index 2f560e82c2..365bbf1a70 100644 --- a/src/Data/List/Fresh/Relation/Unary/All.agda +++ b/src/Data/List/Fresh/Relation/Unary/All.agda @@ -10,7 +10,8 @@ module Data.List.Fresh.Relation.Unary.All where open import Level using (Level; _⊔_; Lift) open import Data.Product.Base using (_×_; _,_; proj₁; uncurry) -open import Data.Sum.Base as Sum using (inj₁; inj₂) +open import Data.Sum.Base as Sum using (inj₁; inj₂; [_,_]′) +open import Function.Base using (_∘_; _$_) open import Relation.Nullary.Decidable as Dec using (Dec; yes; no; _×-dec_) open import Relation.Unary as U open import Relation.Binary.Core using (Rel) @@ -74,6 +75,7 @@ module _ {R : Rel A r} {P : Pred A p} {Q : Pred A q} where decide : Π[ P ∪ Q ] → Π[ All {R = R} P ∪ Any Q ] decide p∪q [] = inj₁ [] - decide p∪q (x ∷# xs) with p∪q x - ... | inj₂ qx = inj₂ (here qx) - ... | inj₁ px = Sum.map (px ∷_) there (decide p∪q xs) + decide p∪q (x ∷# xs) = + [ (λ px → Sum.map (px ∷_) there (decide p∪q xs)) + , inj₂ ∘ here + ]′ $ p∪q x diff --git a/src/Data/List/Kleene/Base.agda b/src/Data/List/Kleene/Base.agda index 8eb83ba864..ef0ca0b0a2 100644 --- a/src/Data/List/Kleene/Base.agda +++ b/src/Data/List/Kleene/Base.agda @@ -11,7 +11,7 @@ module Data.List.Kleene.Base where open import Data.Product.Base as Product using (_×_; _,_; map₂; map₁; proj₁; proj₂) open import Data.Nat.Base as ℕ using (ℕ; suc; zero) -open import Data.Maybe.Base as Maybe using (Maybe; just; nothing) +open import Data.Maybe.Base as Maybe using (Maybe; just; nothing; maybe′) open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂) open import Level using (Level) @@ -137,9 +137,7 @@ module _ (f : A → Maybe B) where mapMaybe+ : A + → B * mapMaybe* : A * → B * - mapMaybe+ (x & xs) with f x - ... | just y = ∹ y & mapMaybe* xs - ... | nothing = mapMaybe* xs + mapMaybe+ (x & xs) = maybe′ (λ y z → ∹ y & z) id (f x) $ mapMaybe* xs mapMaybe* [] = [] mapMaybe* (∹ xs) = mapMaybe+ xs @@ -268,7 +266,7 @@ module _ (f : A → Maybe B → B) where foldrMaybe* [] = nothing foldrMaybe* (∹ xs) = just (foldrMaybe+ xs) - foldrMaybe+ xs = f (head xs) (foldrMaybe* (tail xs)) + foldrMaybe+ (x & xs) = f x (foldrMaybe* xs) ------------------------------------------------------------------------ -- Indexing diff --git a/src/Data/List/NonEmpty/Base.agda b/src/Data/List/NonEmpty/Base.agda index 82f16c270a..0b1793eaf7 100644 --- a/src/Data/List/NonEmpty/Base.agda +++ b/src/Data/List/NonEmpty/Base.agda @@ -203,9 +203,12 @@ snocView (x ∷ .(xs List.∷ʳ y)) | xs List.∷ʳ′ y = (x ∷ xs) ∷ʳ′ y -- The last element in the list. +private + last′ : ∀ {l} → SnocView {A = A} l → A + last′ (_ ∷ʳ′ y) = y + last : List⁺ A → A -last xs with snocView xs -last .(ys ∷ʳ y) | ys ∷ʳ′ y = y +last = last′ ∘ snocView -- Groups all contiguous elements for which the predicate returns the -- same result into lists. The left sums are the ones for which the diff --git a/src/Data/List/Relation/Binary/Infix/Heterogeneous.agda b/src/Data/List/Relation/Binary/Infix/Heterogeneous.agda index b09af201e0..8a5b239eb0 100644 --- a/src/Data/List/Relation/Binary/Infix/Heterogeneous.agda +++ b/src/Data/List/Relation/Binary/Infix/Heterogeneous.agda @@ -49,10 +49,8 @@ map R⇒S (here pref) = here (Prefix.map R⇒S pref) map R⇒S (there inf) = there (map R⇒S inf) toView : ∀ {as bs} → Infix R as bs → View R as bs -toView (here p) with Prefix.toView p -...| inf Prefix.++ suff = MkView [] inf suff -toView (there p) with toView p -... | MkView pref inf suff = MkView (_ ∷ pref) inf suff +toView (here p) with inf Prefix.++ suff ← Prefix.toView p = MkView [] inf suff +toView (there p) with MkView pref inf suff ← toView p = MkView (_ ∷ pref) inf suff fromView : ∀ {as bs} → View R as bs → Infix R as bs fromView (MkView [] inf suff) = here (Prefix.fromView (inf Prefix.++ suff)) diff --git a/src/Data/List/Relation/Binary/Prefix/Heterogeneous.agda b/src/Data/List/Relation/Binary/Prefix/Heterogeneous.agda index 75104bd39e..29a2fb5d02 100644 --- a/src/Data/List/Relation/Binary/Prefix/Heterogeneous.agda +++ b/src/Data/List/Relation/Binary/Prefix/Heterogeneous.agda @@ -53,8 +53,7 @@ module _ {a b r} {A : Set a} {B : Set b} {R : REL A B r} where toView : ∀ {as bs} → Prefix R as bs → PrefixView R as bs toView [] = [] ++ _ - toView (r ∷ rs) with toView rs - ... | rs′ ++ ds = (r ∷ rs′) ++ ds + toView (r ∷ rs) with rs′ ++ ds ← toView rs = (r ∷ rs′) ++ ds fromView : ∀ {as bs} → PrefixView R as bs → Prefix R as bs fromView ([] ++ ds) = [] diff --git a/src/Data/List/Relation/Binary/Suffix/Heterogeneous.agda b/src/Data/List/Relation/Binary/Suffix/Heterogeneous.agda index 441956829f..f15737ada3 100644 --- a/src/Data/List/Relation/Binary/Suffix/Heterogeneous.agda +++ b/src/Data/List/Relation/Binary/Suffix/Heterogeneous.agda @@ -47,8 +47,7 @@ module _ {a b r} {A : Set a} {B : Set b} {R : REL A B r} where toView : ∀ {as bs} → Suffix R as bs → SuffixView R as bs toView (here rs) = [] ++ rs - toView (there {c} suf) with toView suf - ... | cs ++ rs = (c ∷ cs) ++ rs + toView (there {c} suf) with cs ++ rs ← toView suf = (c ∷ cs) ++ rs fromView : ∀ {as bs} → SuffixView R as bs → Suffix R as bs fromView ([] ++ rs) = here rs diff --git a/src/Data/List/Relation/Binary/Suffix/Heterogeneous/Properties.agda b/src/Data/List/Relation/Binary/Suffix/Heterogeneous/Properties.agda index abacb301d0..3506d0000b 100644 --- a/src/Data/List/Relation/Binary/Suffix/Heterogeneous/Properties.agda +++ b/src/Data/List/Relation/Binary/Suffix/Heterogeneous/Properties.agda @@ -40,8 +40,7 @@ module _ {a b r} {A : Set a} {B : Set b} {R : REL A B r} where fromPrefix : ∀ {as bs} → Prefix R as bs → Suffix R (reverse as) (reverse bs) - fromPrefix {as} {bs} p with Prefix.toView p - ... | Prefix._++_ {cs} rs ds = + fromPrefix {as} {bs} p with Prefix._++_ {cs} rs ds ← Prefix.toView p = subst (Suffix R (reverse as)) (sym (List.reverse-++ cs ds)) (Suffix.fromView (reverse ds Suffix.++ Pw.reverse⁺ rs)) @@ -56,8 +55,7 @@ module _ {a b r} {A : Set a} {B : Set b} {R : REL A B r} where toPrefix-rev : ∀ {as bs} → Suffix R as bs → Prefix R (reverse as) (reverse bs) - toPrefix-rev {as} {bs} s with Suffix.toView s - ... | Suffix._++_ cs {ds} rs = + toPrefix-rev {as} {bs} s with Suffix._++_ cs {ds} rs ← Suffix.toView s = subst (Prefix R (reverse as)) (sym (List.reverse-++ cs ds)) (Prefix.fromView (Pw.reverse⁺ rs Prefix.++ reverse cs)) diff --git a/src/Data/List/Relation/Unary/Enumerates/Setoid/Properties.agda b/src/Data/List/Relation/Unary/Enumerates/Setoid/Properties.agda index f1a95b1e14..0f374ea1b5 100644 --- a/src/Data/List/Relation/Unary/Enumerates/Setoid/Properties.agda +++ b/src/Data/List/Relation/Unary/Enumerates/Setoid/Properties.agda @@ -40,8 +40,8 @@ module _ (S : Setoid a ℓ₁) (T : Setoid b ℓ₂) (surj : Surjection S T) whe open Surjection surj map⁺ : ∀ {xs} → IsEnumeration S xs → IsEnumeration T (map to xs) - map⁺ _∈xs y with strictlySurjective y - ... | (x , fx≈y) = ∈-resp-≈ T fx≈y (∈-map⁺ S T cong (x ∈xs)) + map⁺ _∈xs y with (x , fx≈y) ← strictlySurjective y = + ∈-resp-≈ T fx≈y (∈-map⁺ S T cong (x ∈xs)) ------------------------------------------------------------------------ -- _++_ diff --git a/src/Data/Nat/Binary/Subtraction.agda b/src/Data/Nat/Binary/Subtraction.agda index 5ab67ce7c1..1e38de460e 100644 --- a/src/Data/Nat/Binary/Subtraction.agda +++ b/src/Data/Nat/Binary/Subtraction.agda @@ -12,8 +12,8 @@ open import Algebra.Core using (Op₂) open import Algebra.Bundles using (Magma) open import Algebra.Consequences.Propositional using (comm∧distrˡ⇒distrʳ) open import Algebra.Morphism.Consequences using (homomorphic₂-inv) -open import Data.Bool.Base using (true; false) -open import Data.Nat.Base as ℕ using (ℕ) +open import Data.Bool.Base using (true; false; if_then_else_) +open import Data.Nat as ℕ using (ℕ) open import Data.Nat.Binary.Base using (ℕᵇ; 0ᵇ; 2[1+_]; 1+[2_]; double; pred; toℕ; fromℕ; even_; _≤_; _<_; _+_; zero; suc; 1ᵇ; _*_) @@ -53,12 +53,8 @@ zero ∸ _ = 0ᵇ x ∸ zero = x 2[1+ x ] ∸ 2[1+ y ] = double (x ∸ y) 1+[2 x ] ∸ 1+[2 y ] = double (x ∸ y) -2[1+ x ] ∸ 1+[2 y ] with does (x b = a ++ " " ++ b -- it is equal to 0. padLeft : Char → ℕ → String → String -padLeft c n str with n ∸ length str -... | 0 = str -... | l = replicate l c ++ str +padLeft c n str = + let l = n ∸ length str in + if l ≡ᵇ 0 then str else replicate l c ++ str padRight : Char → ℕ → String → String -padRight c n str with n ∸ length str -... | 0 = str -... | l = str ++ replicate l c +padRight c n str = + let l = n ∸ length str in + if l ≡ᵇ 0 then str else str ++ replicate l c padBoth : Char → Char → ℕ → String → String -padBoth cₗ cᵣ n str with n ∸ length str -... | 0 = str -... | l = replicate ⌊ l /2⌋ cₗ ++ str ++ replicate ⌈ l /2⌉ cᵣ +padBoth cₗ cᵣ n str = + let l = n ∸ length str in + if l ≡ᵇ 0 then str else replicate ⌊ l /2⌋ cₗ ++ str ++ replicate ⌈ l /2⌉ cᵣ ------------------------------------------------------------------------ -- Alignment diff --git a/src/Data/Tree/AVL.agda b/src/Data/Tree/AVL.agda index 895a194085..63d6067a9d 100644 --- a/src/Data/Tree/AVL.agda +++ b/src/Data/Tree/AVL.agda @@ -92,13 +92,13 @@ module _ {v} {V : Value v} where headTail : Tree V → Maybe (K& V × Tree V) headTail (tree (Indexed.leaf _)) = nothing - headTail (tree {h = suc _} t) with Indexed.headTail t - ... | (k , _ , _ , t′) = just (k , tree (Indexed.castˡ ⊥⁺<[ _ ] t′)) + headTail (tree {h = suc _} t) with (k , _ , _ , t′) ← Indexed.headTail t + = just (k , tree (Indexed.castˡ ⊥⁺<[ _ ] t′)) initLast : Tree V → Maybe (Tree V × K& V) initLast (tree (Indexed.leaf _)) = nothing - initLast (tree {h = suc _} t) with Indexed.initLast t - ... | (k , _ , _ , t′) = just (tree (Indexed.castʳ t′ [ _ ]<⊤⁺) , k) + initLast (tree {h = suc _} t) with (k , _ , _ , t′) ← Indexed.initLast t + = just (tree (Indexed.castʳ t′ [ _ ]<⊤⁺) , k) foldr : (∀ {k} → Val k → A → A) → A → Tree V → A foldr cons nil (tree t) = Indexed.foldr cons nil t diff --git a/src/Data/Vec.agda b/src/Data/Vec.agda index 2e293acdf9..aa6435e445 100644 --- a/src/Data/Vec.agda +++ b/src/Data/Vec.agda @@ -21,6 +21,7 @@ open import Data.Bool.Base import Data.Nat.Properties as ℕ open import Data.Vec.Bounded.Base as Vec≤ using (Vec≤; ≤-cast; fromVec) +open import Function.Base using (_$_) open import Relation.Nullary open import Relation.Unary @@ -41,18 +42,14 @@ module _ {P : A → Set p} (P? : Decidable P) where filter : ∀ {n} → Vec A n → Vec≤ A n filter [] = Vec≤.[] - filter (a ∷ as) with does (P? a) - ... | true = a Vec≤.∷ filter as - ... | false = ≤-cast (ℕ.n≤1+n _) (filter as) + filter (a ∷ as) = if does (P? a) then a Vec≤.∷_ else ≤-cast (ℕ.n≤1+n _) $ filter as takeWhile : ∀ {n} → Vec A n → Vec≤ A n takeWhile [] = Vec≤.[] - takeWhile (a ∷ as) with does (P? a) - ... | true = a Vec≤.∷ takeWhile as - ... | false = Vec≤.[] + takeWhile (a ∷ as) = if does (P? a) then a Vec≤.∷ takeWhile as else Vec≤.[] dropWhile : ∀ {n} → Vec A n → Vec≤ A n dropWhile Vec.[] = Vec≤.[] - dropWhile (a Vec.∷ as) with does (P? a) - ... | true = ≤-cast (ℕ.n≤1+n _) (dropWhile as) - ... | false = fromVec (a Vec.∷ as) + dropWhile (a Vec.∷ as) = + if does (P? a) then ≤-cast (ℕ.n≤1+n _) (dropWhile as) + else fromVec (a Vec.∷ as) diff --git a/src/Data/Vec/Base.agda b/src/Data/Vec/Base.agda index 5f57c22b2f..8c03fb8a83 100644 --- a/src/Data/Vec/Base.agda +++ b/src/Data/Vec/Base.agda @@ -14,7 +14,7 @@ open import Data.Fin.Base using (Fin; zero; suc) open import Data.List.Base as List using (List) open import Data.Product.Base as Product using (∃; ∃₂; _×_; _,_; proj₁; proj₂) open import Data.These.Base as These using (These; this; that; these) -open import Function.Base using (const; _∘′_; id; _∘_) +open import Function.Base using (const; _∘′_; id; _∘_; _$_) open import Level using (Level) open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; trans; cong) open import Relation.Nullary.Decidable.Core using (does; T?) @@ -232,9 +232,7 @@ sum = foldr _ _+_ 0 count : ∀ {P : Pred A p} → Decidable P → Vec A n → ℕ count P? [] = zero -count P? (x ∷ xs) with does (P? x) -... | true = suc (count P? xs) -... | false = count P? xs +count P? (x ∷ xs) = if does (P? x) then suc else id $ count P? xs countᵇ : (A → Bool) → Vec A n → ℕ countᵇ p = count (T? ∘ p) diff --git a/src/Data/Vec/Membership/Setoid.agda b/src/Data/Vec/Membership/Setoid.agda index 72e57e15f3..cfa69e591b 100644 --- a/src/Data/Vec/Membership/Setoid.agda +++ b/src/Data/Vec/Membership/Setoid.agda @@ -51,9 +51,8 @@ _∷=_ {xs = xs} x∈xs v = xs Vec.[ index x∈xs ]≔ v module _ {p} {P : Pred A p} where find : ∀ {n} {xs : Vec A n} → Any P xs → ∃ λ x → x ∈ xs × P x - find (here px) = (_ , here refl , px) - find (there pxs) with find pxs - ... | (x , x∈xs , px) = (x , there x∈xs , px) + find (here px) = _ , here refl , px + find (there pxs) = let x , x∈xs , px = find pxs in x , there x∈xs , px lose : P Respects _≈_ → ∀ {x n} {xs : Vec A n} → x ∈ xs → P x → Any P xs lose resp x∈xs px = Any.map (flip resp px) x∈xs diff --git a/src/Relation/Binary/Construct/NaturalOrder/Left.agda b/src/Relation/Binary/Construct/NaturalOrder/Left.agda index 47465e8926..cd8864af6e 100644 --- a/src/Relation/Binary/Construct/NaturalOrder/Left.agda +++ b/src/Relation/Binary/Construct/NaturalOrder/Left.agda @@ -9,7 +9,7 @@ open import Algebra.Core open import Data.Product.Base using (_,_; _×_) -open import Data.Sum.Base using (inj₁; inj₂) +open import Data.Sum.Base using (inj₁; inj₂; map) open import Relation.Binary.Core using (Rel; _⇒_) open import Relation.Binary.Bundles using (Preorder; Poset; DecPoset; TotalOrder; DecTotalOrder) @@ -58,9 +58,7 @@ antisym isEq comm {x} {y} x≤y y≤x = begin where open IsEquivalence isEq; open ≈-Reasoning (record { isEquivalence = isEq }) total : Symmetric _≈_ → Transitive _≈_ → Selective _∙_ → Commutative _∙_ → Total _≤_ -total sym trans sel comm x y with sel x y -... | inj₁ x∙y≈x = inj₁ (sym x∙y≈x) -... | inj₂ x∙y≈y = inj₂ (sym (trans (comm y x) x∙y≈y)) +total sym trans sel comm x y = map sym (λ x∙y≈y → trans (sym x∙y≈y) (comm x y)) (sel x y) trans : IsSemigroup _∙_ → Transitive _≤_ trans semi {x} {y} {z} x≤y y≤z = begin diff --git a/src/Relation/Binary/Construct/NaturalOrder/Right.agda b/src/Relation/Binary/Construct/NaturalOrder/Right.agda index 76529350e2..024b946cc8 100644 --- a/src/Relation/Binary/Construct/NaturalOrder/Right.agda +++ b/src/Relation/Binary/Construct/NaturalOrder/Right.agda @@ -9,7 +9,7 @@ open import Algebra.Core using (Op₂) open import Data.Product.Base using (_,_; _×_) -open import Data.Sum.Base using (inj₁; inj₂) +open import Data.Sum.Base using (inj₁; inj₂; map) open import Relation.Binary.Core using (Rel; _⇒_) open import Relation.Binary.Bundles using (Preorder; Poset; DecPoset; TotalOrder; DecTotalOrder) @@ -58,9 +58,8 @@ antisym isEq comm {x} {y} x≤y y≤x = begin where open ≈-Reasoning (record { isEquivalence = isEq }) total : Symmetric _≈_ → Transitive _≈_ → Selective _∙_ → Commutative _∙_ → Total _≤_ -total sym trans sel comm x y with sel x y -... | inj₁ x∙y≈x = inj₁ (trans (sym x∙y≈x) (comm x y) ) -... | inj₂ x∙y≈y = inj₂ (sym x∙y≈y) +total sym trans sel comm x y = + map (λ x∙y≈x → trans (sym x∙y≈x) (comm x y)) sym (sel x y) trans : IsSemigroup _∙_ → Transitive _≤_ trans semi {x} {y} {z} x≤y y≤z = begin diff --git a/src/Text/Pretty/Core.agda b/src/Text/Pretty/Core.agda index 9a157ddda2..6883054ae8 100644 --- a/src/Text/Pretty/Core.agda +++ b/src/Text/Pretty/Core.agda @@ -145,8 +145,8 @@ private pad : Maybe String pad with x.lastWidth - ... | 0 = nothing - ... | l = just (replicate l ' ') + ... | 0 = nothing + ... | l@(suc _) = just (replicate l ' ') size-pad : maybe′ length 0 pad ≡ x.lastWidth size-pad with x.lastWidth