restored Id to String

src/Maps.lagda

@@ -36,7 +36,7 @@ standard library, wherever they overlap.
 open import Data.Nat         using (ℕ)
 open import Data.Empty       using (⊥; ⊥-elim)
 open import Data.Maybe       using (Maybe; just; nothing)
--- open import Data.String      using (String)
+open import Data.String      using (String)
 open import Relation.Nullary using (¬_; Dec; yes; no)
 open import Relation.Binary.PropositionalEquality
                              using (_≡_; refl; _≢_; trans; sym)
@@ -54,8 +54,7 @@ we repeat its definition here.
 
 \begin{code}
 data Id : Set where
-  -- id : String → Id
+  id : String → Id
-  id : ℕ → Id
 \end{code}
 
 We recall a standard fact of logic.
@@ -70,7 +69,7 @@ by deciding equality on the underlying strings.
 
 \begin{code}
 _≟_ : (x y : Id) → Dec (x ≡ y)
-id x ≟ id y with x Data.Nat.≟ y -- x Data.String.≟ 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 (contrapositive id-inj x≢y)
   where
@@ -82,9 +81,9 @@ We define some identifiers for future use.
 
 \begin{code}
 x y z : Id
-x = id 0 -- "x"
+x = id "x"
-y = id 1 -- "y"
+y = id "y"
-z = id 2 -- "z"
+z = id "z"
 \end{code}
 
 ## Total Maps

src/Stlc.lagda

@@ -45,9 +45,9 @@ data Term : Set where
 Some examples.
 \begin{code}
 f x y : Id
-f  =  id 0 -- "f"
+f  =  id "f"
-x  =  id 1 -- "x"
+x  =  id "x"
-y  =  id 2 -- "y"
+y  =  id "y"
 
 I[𝔹] I[𝔹⇒𝔹] K[𝔹][𝔹] not[𝔹] : Term 
 I[𝔹]  =  (λᵀ x ∈ 𝔹 ⇒ (varᵀ x))