updated stlc

Stlc.lagda

@@ -11,7 +11,6 @@ permalink     : "sf/Stlc.html"
 module Stlc where
 \end{code}
 
-<div class="hidden">
 \begin{code}
 open import Maps using (Id; id; _≟_; PartialMap; module PartialMap)
 open import Data.Empty using (⊥; ⊥-elim)
@@ -22,7 +21,6 @@ open import Function using (_∘_; _$_)
 open import Relation.Nullary using (Dec; yes; no)
 open import Relation.Binary.PropositionalEquality using (_≡_; _≢_; refl)
 \end{code}
-</div>
 
 # The Simply Typed Lambda-Calculus
 
@@ -164,13 +162,9 @@ so we will STLC's function type as `_⇒_`.
 data Type : Set where
   bool : Type
   _⇒_  : Type → Type → Type
-\end{code}
 
-<div class="hidden">
-\begin{code}
 infixr 5 _⇒_
 \end{code}
-</div>
 
 
 ### Terms
@@ -197,21 +191,20 @@ to Agda (and other functional languages like ML, Haskell, etc.),
 which use _type inference_ to fill in missing annotations.  We're
 not considering type inference here.
 
-Some examples...
+We introduce $$x, y, z$$ as names for variables.  The pragmas ensure
+that $$id 0, id 1, id 2$$ display as $$x, y, z$$.
 
 \begin{code}
 x = id 0
 y = id 1
 z = id 2
-\end{code}
 
-<div class="hidden">
-\begin{code}
 {-# DISPLAY zero = x #-}
 {-# DISPLAY suc zero = y #-}
 {-# DISPLAY suc (suc zero) = z #-}
 \end{code}
-</div>
+
+Some examples...
 
 $$\text{idB} = \lambda x:bool. x$$.