From 65d9e7cdfd921d171594d91f3de10cf6cd1f3c14 Mon Sep 17 00:00:00 2001 From: wadler Date: Tue, 20 Jun 2017 14:35:24 +0100 Subject: [PATCH] updated Maps --- src/Maps.lagda | 20 +++++++++++++------- 1 file changed, 13 insertions(+), 7 deletions(-) diff --git a/src/Maps.lagda b/src/Maps.lagda index 941f7c1f..e5a2996f 100644 --- a/src/Maps.lagda +++ b/src/Maps.lagda @@ -49,27 +49,33 @@ Documentation for the standard library can be found at ## Identifiers First, we need a type for the keys that we use to index into our -maps. For this purpose, we again use the type Id` from the +maps. For this purpose, we again use the type `Id` from the [Lists](sf/Lists.html) chapter. To make this chapter self contained, -we repeat its definition here, together with the equality comparison -function for ids and its fundamental property. +we repeat its definition here. \begin{code} data Id : Set where id : String → Id \end{code} +We recall a standard fact of logic. + +\begin{code} +contrapositive : ∀ {ℓ₁ ℓ₂} {P : Set ℓ₁} {Q : Set ℓ₂} → (P → Q) → (¬ Q → ¬ P) +contrapositive p→q ¬q p = ¬q (p→q p) +\end{code} + +Using the above, we can decide equality of two identifiers +by deciding equality on the underlying strings. + \begin{code} _≟_ : (x y : Id) → Dec (x ≡ y) id x ≟ id y with x Data.String.≟ y id x ≟ id y | yes refl = yes refl -id x ≟ id y | no x≠y = no (x≠y ∘ id-inj) +id x ≟ id y | no x≢y = no (contrapositive id-inj x≢y) where id-inj : ∀ {x y} → id x ≡ id y → x ≡ y id-inj refl = refl - --- contrapositive : ∀ {P Q} → (P → Q) → (¬ Q → ¬ P) --- contrapositive p→q ¬q p = ¬q (p→q p) \end{code} We define some identifiers for future use.