reorganize equality imports

Since we are working with multiple setoids now, it makes more sense to
qualify their members. Follow the "as P" pattern from the standard
library. Also stop importing those symbols from Relation.Binary.Core as
later agda-stdlib versions will move them away. Rather than EqSetoid or
PropEq, use P.setoid consistently.

1 files changed, 9 insertions, 9 deletions

diff --git a/Examples.agda b/Examples.agda
index bedad5a..a36ba3a 100644
--- a/Examples.agda
+++ b/Examples.agda
@@ -8,7 +8,7 @@ open import Data.List using (List ; length) renaming ([] to []L ; _∷_ to _∷L
 open import Data.Vec using (Vec ; [] ; _∷_ ; reverse ; _++_ ; tail ; take ; drop ; map)
 open import Function using (id)
 import Relation.Binary
-open import Relation.Binary.PropositionalEquality using (_≡_ ; refl ; cong)
+open import Relation.Binary.PropositionalEquality as P using (_≡_)
 
 open import Structures using (Shaped)
 import GetTypes
@@ -40,7 +40,7 @@ tail' : Get
 tail' = assume-get suc id tail
 
 tail-example : bff ℕ-decSetoid tail' 2 (8 ∷ 5 ∷ []) (3 ∷ 1 ∷ []) ≡ just (just 8 ∷ just 3 ∷ just 1 ∷ [])
-tail-example = refl
+tail-example = P.refl
 
 take' : ℕ → Get
 take' n = assume-get (_+_ n) _ (take n)
@@ -56,7 +56,7 @@ sieve' = assume-get id _ f
         f (x ∷ _ ∷ xs) = x ∷ f xs
 
 sieve-example : bff ℕ-decSetoid sieve' 4 (0 ∷ 2 ∷ []) (1 ∷ 3 ∷ []) ≡ just (just 1 ∷ just 2 ∷ just 3 ∷ nothing ∷ [])
-sieve-example = refl
+sieve-example = P.refl
 
 intersperse-len : ℕ → ℕ
 intersperse-len zero          = zero
@@ -74,10 +74,10 @@ intersperse' = assume-get suc intersperse-len f
         f (s ∷ v)        = intersperse s v
 
 intersperse-neg-example : bff ℕ-decSetoid intersperse' 3 (0 ∷ []) (1 ∷ 2 ∷ 3 ∷ 4 ∷ 5 ∷ []) ≡ nothing
-intersperse-neg-example = refl
+intersperse-neg-example = P.refl
 
 intersperse-pos-example : bff ℕ-decSetoid intersperse' 3 (0 ∷ []) (1 ∷ 2 ∷ 3 ∷ 2 ∷ 5 ∷ []) ≡ just (map just (2 ∷ 1 ∷ 3 ∷ 5 ∷ []))
-intersperse-pos-example = refl
+intersperse-pos-example = P.refl
 
 data PairVec (α : Set) (β : Set) : List α → Set where
   []P : PairVec α β []L
@@ -101,9 +101,9 @@ PairVecFirstShaped α = record
         fill (a ∷L s) (b ∷ v) = a , b ∷P fill s v
 
         content-fill : {β : Set} {s : List α} → (p : PairVec α β s) → fill s (content p) ≡ p
-        content-fill []P          = refl
-        content-fill (a , b ∷P p) = cong (_,_∷P_ a b) (content-fill p)
+        content-fill []P          = P.refl
+        content-fill (a , b ∷P p) = P.cong (_,_∷P_ a b) (content-fill p)
 
         fill-content : {β : Set} → (s : List α) → (v : Vec β (length s)) → content (fill s v) ≡ v
-        fill-content []L      []      = refl
-        fill-content (a ∷L s) (b ∷ v) = cong (_∷_ b) (fill-content s v)
+        fill-content []L      []      = P.refl
+        fill-content (a ∷L s) (b ∷ v) = P.cong (_∷_ b) (fill-content s v)