From c835e655a05c73f7dd2dc46c652be3d43e91a4b7 Mon Sep 17 00:00:00 2001
From: Helmut Grohne <helmut@subdivi.de>
Date: Sun, 25 Nov 2018 10:35:23 +0100
Subject: 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.
---
 Examples.agda | 18 +++++++++---------
 1 file changed, 9 insertions(+), 9 deletions(-)

(limited to 'Examples.agda')

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)
-- 
cgit v1.2.3