diff options
Diffstat (limited to 'Examples.agda')
| -rw-r--r-- | Examples.agda | 18 |
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) |