Revising Bin

src/plfa/Fonts.lagda.md

@@ -53,8 +53,8 @@ ABCDEFGHIJKLMNOPQRSTUVWXYZ|
 ∧∧∨∨|
 ⊗⊗⊗⊗|
 ⊔⊔⊔⊔|
-ᶜᶜᵇᵇ|
-ˡˡʳʳ|
+cᶜbᵇ|
+lˡrʳ|
 ⁻⁻⁺⁺|
 ℕℕℕℕ|
 ∀∀∃∃|

src/plfa/part1/Induction.lagda.md

@@ -955,24 +955,18 @@ for all `m`, `n`, and `p`.
 
 Recall that
 Exercise [Bin]({{ site.baseurl }}/Naturals/#Bin)
-defines a datatype of bitstrings representing natural numbers
-```
-data Bin : Set where
-  nil : Bin
-  x0_ : Bin → Bin
-  x1_ : Bin → Bin
-```
+defines a datatype `Bin` of bitstrings representing natural numbers,
 and asks you to define functions
 
     inc   : Bin → Bin
     to    : ℕ → Bin
     from  : Bin → ℕ
 
-Consider the following laws, where `n` ranges over naturals and `x`
+Consider the following laws, where `n` ranges over naturals and `b`
 over bitstrings:
 
-    from (inc x) ≡ suc (from x)
-    to (from x) ≡ x
+    from (inc b) ≡ suc (from b)
+    to (from b) ≡ b
     from (to n) ≡ n
 
 For each law: if it holds, prove; if not, give a counterexample.

src/plfa/part1/Isomorphism.lagda.md

@@ -471,14 +471,8 @@ Show that equivalence is reflexive, symmetric, and transitive.
 Recall that Exercises
 [Bin]({{ site.baseurl }}/Naturals/#Bin) and
 [Bin-laws]({{ site.baseurl }}/Induction/#Bin-laws)
-define a datatype of bitstrings representing natural numbers:
-```
-data Bin : Set where
-  nil : Bin
-  x0_ : Bin → Bin
-  x1_ : Bin → Bin
-```
-And ask you to define the following functions
+define a datatype `Bin` of bitstrings representing natural numbers,
+and asks you to define the following functions and predicates:
 
     to : ℕ → Bin
     from : Bin → ℕ

src/plfa/part1/Naturals.lagda.md

@@ -877,22 +877,22 @@ A more efficient representation of natural numbers uses a binary
 rather than a unary system.  We represent a number as a bitstring:
 ```
 data Bin : Set where
-  nil : Bin
-  x0_ : Bin → Bin
-  x1_ : Bin → Bin
+  ⟨⟩ : Bin
+  _O : Bin → Bin
+  _I : Bin → Bin
 ```
 For instance, the bitstring
 
     1011
 
-standing for the number eleven is encoded, right to left, as
+standing for the number eleven is encoded as
 
-    x1 x1 x0 x1 nil
+    ⟨⟩ I O I I
 
 Representations are not unique due to leading zeros.
 Hence, eleven is also represented by `001011`, encoded as:
 
-    x1 x1 x0 x1 x0 x0 nil
+    ⟨⟩ O I O I I
 
 Define a function
 
@@ -901,7 +901,7 @@ Define a function
 that converts a bitstring to the bitstring for the next higher
 number.  For example, since `1100` encodes twelve, we should have:
 
-    inc (x1 x1 x0 x1 nil) ≡ x0 x0 x1 x1 nil
+    inc (⟨⟩ I O I I) ≡ ⟨⟩ I I O O
 
 Confirm that this gives the correct answer for the bitstrings
 encoding zero through four.

src/plfa/part1/Quantifiers.lagda.md

@@ -435,14 +435,8 @@ Recall that Exercises
 [Bin]({{ site.baseurl }}/Naturals/#Bin),
 [Bin-laws]({{ site.baseurl }}/Induction/#Bin-laws), and
 [Bin-predicates]({{ site.baseurl }}/Relations/#Bin-predicates)
-define a datatype of bitstrings representing natural numbers:
-```
-data Bin : Set where
-  nil : Bin
-  x0_ : Bin → Bin
-  x1_ : Bin → Bin
-```
-And ask you to define the following functions and predicates:
+define a datatype `Bin` of bitstrings representing natural numbers,
+and asks you to define the following functions and predicates:
 
     to   : ℕ → Bin
     from : Bin → ℕ
@@ -455,12 +449,12 @@ And to establish the following properties:
     ----------
     Can (to n)
 
-    Can x
+    Can b
     ---------------
-    to (from x) ≡ x
+    to (from b) ≡ b
 
 Using the above, establish that there is an isomorphism between `ℕ` and
-`∃[ x ](Can x)`.
+`∃[ b ](Can b)`.
 
 ```
 -- Your code goes here

src/plfa/part1/Relations.lagda.md

@@ -753,8 +753,8 @@ defines a datatype `Bin` of bitstrings representing natural numbers.
 Representations are not unique due to leading zeros.
 Hence, eleven may be represented by both of the following:
 
-    x1 x1 x0 x1 nil
-    x1 x1 x0 x1 x0 x0 nil
+    ⟨⟩ I O I I
+    ⟨⟩ O O I O I I
 
 Define a predicate
 
@@ -775,7 +775,7 @@ Show that increment preserves canonical bitstrings:
 
     Can x
     ------------
-    Can (inc x)
+    Can (inc b)
 
 Show that converting a natural to a bitstring always yields a
 canonical bitstring:
@@ -786,9 +786,9 @@ canonical bitstring:
 Show that converting a canonical bitstring to a natural
 and back is the identity:
 
-    Can x
+    Can b
     ---------------
-    to (from x) ≡ x
+    to (from b) ≡ b
 
 (Hint: For each of these, you may first need to prove related
 properties of `One`.)