From 6ce567bf63a61bce4ccf71e3ec402d94d1da2fb1 Mon Sep 17 00:00:00 2001 From: Helmut Grohne Date: Sun, 29 Sep 2019 13:54:46 +0200 Subject: port to agda/2.6.0.1 and agda-stdlib/1.1 * Data.Vec.lookup changed parameter order. * A number of symbols were moved from Data.Maybe to submodules. * In a number of occasions, agda no longer figures implicit arguments and they had to be made explicit. * We can no longer use heterogeneous proofs inside equational reasoning for propositional equality. Use heterogeneous equational reasoning. * Stop importing proof-irrelevance as that would require K. --- LiftGet.agda | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'LiftGet.agda') diff --git a/LiftGet.agda b/LiftGet.agda index 4ddf26f..e0a6932 100644 --- a/LiftGet.agda +++ b/LiftGet.agda @@ -8,7 +8,7 @@ open import Data.List using (List ; [] ; _∷_ ; length ; replicate ; map) open import Data.List.Properties using (length-map ; length-replicate) open import Data.Product using (∃ ; _,_ ; proj₁ ; proj₂) open import Function using (_∘_ ; flip ; const) -open import Relation.Binary.PropositionalEquality as P using (_≡_ ; _≗_ ; proof-irrelevance ; module ≡-Reasoning) +open import Relation.Binary.PropositionalEquality as P using (_≡_ ; _≗_ ; module ≡-Reasoning) open import Relation.Binary.HeterogeneousEquality as H using (module ≅-Reasoning ; _≅_ ; ≅-to-≡ ; ≡-to-≅ ; ≡-subst-removable) import FreeTheorems @@ -30,16 +30,16 @@ toList∘map f (x ∷V xs) = P.cong (_∷_ (f x)) (toList∘map f xs) GetV-to-GetL : GetV → GetL GetV-to-GetL getrecord = record { get = toList ∘ get ∘ fromList; free-theorem = ft } where open GetV getrecord - open ≡-Reasoning + open ≅-Reasoning ft : {α β : Set} → (f : α → β) → (xs : List α) → toList (get (fromList (map f xs))) ≡ map f (toList (get (fromList xs))) - ft f xs = begin + ft f xs = ≅-to-≡ (begin toList (get (fromList (map f xs))) ≅⟨ H.cong₂ {B = Vec _} (λ n → toList ∘ get) (H.reflexive (length-map f xs)) (fromList∘map f xs) ⟩ toList (get (mapV f (fromList xs))) ≡⟨ P.cong toList (free-theorem f (fromList xs)) ⟩ toList (mapV f (get (fromList xs))) ≡⟨ toList∘map f (get (fromList xs)) ⟩ - map f (toList (get (fromList xs))) ∎ + map f (toList (get (fromList xs))) ∎) getList-to-getlen : get-type → ℕ → ℕ getList-to-getlen get = length ∘ get ∘ flip replicate tt -- cgit v1.2.3