Make \prime apostrophe usage consistent (change to prime) (part 2, local identifiers) (#1205)

* Replace apostrophes with \prime in local identifiers across the library

Author: elsanussi-s-mneina

README/Case.agda

@@ -57,7 +57,7 @@ div2 : ℕ → ℕ
 div2 zero    = zero
 div2 (suc m) = case m of λ where
   zero     → zero
-  (suc m') → suc (div2 m')
+  (suc m′) → suc (div2 m′)
 
 
 -- Note that some natural uses of case are rejected by the termination

README/Data/List/Relation/Ternary/Interleaving.agda

@@ -73,12 +73,12 @@ module _ {a p} {A : Set a} {P : Pred A p} (P? : Decidable P) where
   filter []       = [] ≡ [] ⊎ []
   filter (x ∷ xs) =
     -- otherwise we start by running filter on the tail
-    let xs' ≡ ps ⊎ ¬ps = filter xs in
+    let xs′ ≡ ps ⊎ ¬ps = filter xs in
     -- And depending on whether `P` holds of the head,
     -- we cons it to the `kept` or `thrown` list.
     case P? x of λ where -- [1]
-      (yes p) → consˡ xs' ≡ p ∷ ps ⊎      ¬ps
-      (no ¬p) → consʳ xs' ≡     ps ⊎ ¬p ∷ ¬ps
+      (yes p) → consˡ xs′ ≡ p ∷ ps ⊎      ¬ps
+      (no ¬p) → consʳ xs′ ≡     ps ⊎ ¬p ∷ ¬ps
 
 
 

README/Data/Tree/AVL.agda

@@ -24,8 +24,8 @@ open import Data.String using (String)
 open import Data.Vec using (Vec; _∷_; [])
 open import Relation.Binary.PropositionalEquality
 
-open Data.Tree.AVL <-strictTotalOrder renaming (Tree to Tree')
-Tree = Tree' (MkValue (Vec String) (subst (Vec String)))
+open Data.Tree.AVL <-strictTotalOrder renaming (Tree to Tree′)
+Tree = Tree′ (MkValue (Vec String) (subst (Vec String)))
 
 ------------------------------------------------------------------------
 -- Construction of trees

README/Debug/Trace.agda

@@ -46,8 +46,8 @@ div m n    = just (go m m) where
   go : (fuel : ℕ) (m : ℕ) → ℕ
   go zero       m = trace ("Invariant: " ++ show m ++ " should be zero.") zero
   go (suc fuel) m =
-    let m' = trace ("Thunk for step " ++ show fuel ++ " forced") (m ∸ n) in
-    trace ("Recursive call for step " ++ show fuel) (suc (go fuel m'))
+    let m′ = trace ("Thunk for step " ++ show fuel ++ " forced") (m ∸ n) in
+    trace ("Recursive call for step " ++ show fuel) (suc (go fuel m′))
 
 -- To observe the behaviour of this code, we need to compile it and run it.
 -- To run it, we need a main function. We define a very basic one: run div,

README/Nary.agda

@@ -147,8 +147,8 @@ curry₁ = curryₙ 4
 -- to be right nested. Which means that if you have a deeply-nested product
 -- then it won't be affected by the procedure.
 
-curry₁' : (A × (B × C) × D → E) → A → (B × C) → D → E
-curry₁' = curryₙ 3
+curry₁′ : (A × (B × C) × D → E) → A → (B × C) → D → E
+curry₁′ = curryₙ 3
 
 -- When we are currying a function, we have no obligation to pass its exact
 -- arity as the parameter: we can decide to only curry part of it like so:
@@ -174,8 +174,8 @@ proj₃ = projₙ 5 (# 2)
 -- passing `projₙ` a natural number which is smaller than the size of the
 -- n-ary product, seeing (A₁ × ⋯ × Aₙ) as (A₁ × ⋯ × (Aₖ × ⋯ × Aₙ)).
 
-proj₃' : (A × B × C × D × E) → C × D × E
-proj₃' = projₙ 3 (# 2)
+proj₃′ : (A × B × C × D × E) → C × D × E
+proj₃′ = projₙ 3 (# 2)
 
 -----------------------------------------------------------------------
 -- insertₙ : ∀ n (k : Fin (suc n)) →
@@ -184,8 +184,8 @@ proj₃' = projₙ 3 (# 2)
 insert₁ : C → (A × B × D × E) → (A × B × C × D × E)
 insert₁ = insertₙ 4 (# 2)
 
-insert₁' : C → (A × B × D × E) → (A × B × C × D × E)
-insert₁' = insertₙ 3 (# 2)
+insert₁′ : C → (A × B × D × E) → (A × B × C × D × E)
+insert₁′ = insertₙ 3 (# 2)
 
 -- Note that `insertₙ` takes a `Fin (suc n)`. Indeed in an n-ary product
 -- there are (suc n) positions at which one may insert a value. We may
@@ -248,10 +248,10 @@ compose₁ f = 1 %= f ⊢ replicate
 -- Here we spell out the equivalent explicit variable-manipulation and
 -- prove the two functions equal.
 
-compose₁' : (A → B) → ℕ → A → List B
-compose₁' f n a = replicate n (f a)
+compose₁′ : (A → B) → ℕ → A → List B
+compose₁′ f n a = replicate n (f a)
 
-compose₁-eq : compose₁ {a} {A} {b} {B} ≡ compose₁'
+compose₁-eq : compose₁ {a} {A} {b} {B} ≡ compose₁′
 compose₁-eq = refl
 
 -----------------------------------------------------------------------

src/Algebra/Properties/BooleanAlgebra.agda

@@ -437,7 +437,7 @@ module XorRing
       ((x ∨ y) ∧ (¬ x ∨ ¬ y)) ∨ z        ≈˘⟨ ∨-congʳ $ ∧-congˡ (deMorgan₁ _ _) ⟩
       ((x ∨ y) ∧ ¬ (x ∧ y)) ∨ z          ∎
 
-    lem₂' = begin
+    lem₂′ = begin
       (x ∨ ¬ y) ∧ (¬ x ∨ y)              ≈˘⟨ ∧-identityˡ _ ⟨ ∧-cong ⟩ ∧-identityʳ _ ⟩
       (⊤ ∧ (x ∨ ¬ y)) ∧ ((¬ x ∨ y) ∧ ⊤)  ≈˘⟨  (∨-complementˡ _ ⟨ ∧-cong ⟩ ∨-comm _ _)
                                                 ⟨ ∧-cong ⟩
@@ -450,7 +450,7 @@ module XorRing
 
     lem₂ = begin
       ((x ∨ ¬ y) ∨ ¬ z) ∧ ((¬ x ∨ y) ∨ ¬ z)  ≈˘⟨ ∨-∧-distribʳ _ _ _ ⟩
-      ((x ∨ ¬ y) ∧ (¬ x ∨ y)) ∨ ¬ z          ≈⟨ ∨-congʳ lem₂' ⟩
+      ((x ∨ ¬ y) ∧ (¬ x ∨ y)) ∨ ¬ z          ≈⟨ ∨-congʳ lem₂′ ⟩
       ¬ ((x ∨ y) ∧ ¬ (x ∧ y)) ∨ ¬ z          ≈˘⟨ deMorgan₁ _ _ ⟩
       ¬ (((x ∨ y) ∧ ¬ (x ∧ y)) ∧ z)          ∎
 
@@ -460,7 +460,7 @@ module XorRing
       (x ∨ (y ∨ z)) ∧ (x ∨ (¬ y ∨ ¬ z))  ≈˘⟨ ∨-assoc _ _ _ ⟨ ∧-cong ⟩ ∨-assoc _ _ _ ⟩
       ((x ∨ y) ∨ z) ∧ ((x ∨ ¬ y) ∨ ¬ z)  ∎
 
-    lem₄' = begin
+    lem₄′ = begin
       ¬ ((y ∨ z) ∧ ¬ (y ∧ z))    ≈⟨ deMorgan₁ _ _ ⟩
       ¬ (y ∨ z) ∨ ¬ ¬ (y ∧ z)    ≈⟨ deMorgan₂ _ _ ⟨ ∨-cong ⟩ ¬-involutive _ ⟩
       (¬ y ∧ ¬ z) ∨ (y ∧ z)      ≈⟨ lemma₂ _ _ _ _ ⟩
@@ -474,7 +474,7 @@ module XorRing
 
     lem₄ = begin
       ¬ (x ∧ ((y ∨ z) ∧ ¬ (y ∧ z)))  ≈⟨ deMorgan₁ _ _ ⟩
-      ¬ x ∨ ¬ ((y ∨ z) ∧ ¬ (y ∧ z))  ≈⟨ ∨-congˡ lem₄' ⟩
+      ¬ x ∨ ¬ ((y ∨ z) ∧ ¬ (y ∧ z))  ≈⟨ ∨-congˡ lem₄′ ⟩
       ¬ x ∨ ((y ∨ ¬ z) ∧ (¬ y ∨ z))  ≈⟨ ∨-∧-distribˡ _ _ _ ⟩
       (¬ x ∨ (y     ∨ ¬ z)) ∧
       (¬ x ∨ (¬ y ∨ z))              ≈˘⟨ ∨-assoc _ _ _ ⟨ ∧-cong ⟩ ∨-assoc _ _ _ ⟩

src/Category/Monad/Continuation.agda

@@ -58,7 +58,7 @@ DContTIMonadDCont : ∀ (K : I → Set f) {M} →
 DContTIMonadDCont K Mon = record
   { monad = DContTIMonad K Mon
   ; reset = λ e k → e return >>= k
-  ; shift = λ e k → e (λ a k' → (k a) >>= k') return
+  ; shift = λ e k → e (λ a k′ → (k a) >>= k′) return
   }
   where
   open RawIMonad Mon

src/Category/Monad/Indexed.agda

@@ -48,7 +48,7 @@ record RawIMonad {I : Set i} (M : IFun I f) : Set (i ⊔ suc f) where
   rawIApplicative : RawIApplicative M
   rawIApplicative = record
     { pure = return
-    ; _⊛_  = λ f x → f >>= λ f' → x >>= λ x' → return (f' x')
+    ; _⊛_  = λ f x → f >>= λ f′ → x >>= λ x′ → return (f′ x′)
     }
 
   open RawIApplicative rawIApplicative public

src/Codata/Cowriter.agda

@@ -113,7 +113,7 @@ _>>=_ : ∀ {i} → Cowriter W A i → (A → Cowriter W X i) → Cowriter W X i
 
 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₁ (w , seed′) = w ∷ λ where .force → unfold next seed′
 ... | inj₂ a           = [ a ]
 
 

src/Data/DifferenceList.agda

@@ -72,10 +72,10 @@ map f xs = λ k → List.map f (toList xs) ⟨ List._++_ ⟩ k
 -- concat is linear in the length of the outer list.
 
 concat : DiffList (DiffList A) → DiffList A
-concat xs = concat' (toList xs)
+concat xs = concat′ (toList xs)
   where
-  concat' : List (DiffList A) → DiffList A
-  concat' = List.foldr _++_ []
+  concat′ : List (DiffList A) → DiffList A
+  concat′ = List.foldr _++_ []
 
 take : ℕ → DiffList A → DiffList A
 take n = lift (List.take n)