A number of with are not really needed (#2363)

* a number of 'with' are not really needed. Many, many more were, so left as is.

* whitespace

* deal with a few outstanding comments.

* actually re-introduce a 'with' as it is actually clearer.

* with fits better here too.

* tweak things a little from review by James.

* Update src/Codata/Sized/Cowriter.agda

layout for readability

Co-authored-by: G. Allais <[email protected]>

* Update src/Data/Fin/Base.agda

layout for readability

Co-authored-by: G. Allais <[email protected]>

* Update src/Data/List/Fresh/Relation/Unary/All.agda

layout for readability

Co-authored-by: G. Allais <[email protected]>

---------

Co-authored-by: G. Allais <[email protected]>

Author: 2 people

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)

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

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

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)

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

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,29 +161,28 @@ 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
   ... | false = _
 
   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

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

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

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

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))