[Switched to ordinary ℕ and Vec instead of the variants based on star-lists.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20080513193052
 + Since the code becomes a bit easier to understand.
] hunk ./ApplicationBased.agda 10
+open import Data.Nat
+open import Data.Vec
hunk ./ApplicationBased.agda 13
-open import Data.Star.Nat
-open import Data.Star.Vec
-open import Data.Star.Decoration
hunk ./ApplicationBased.agda 37
-  a ^ ε       = a
-  a ^ (_ ◅ n) = a -> a ^ n
+  a ^ zero  = a
+  a ^ suc n = a -> a ^ n
hunk ./ApplicationBased.agda 40
-  return : ℕ -> ℕ ^ 0#
+  return : ℕ -> ℕ ^ 0
hunk ./ApplicationBased.agda 43
-  sub : ℕ ^ 2#
+  sub : ℕ ^ 2
hunk ./ApplicationBased.agda 46
-  _<$_$>_ : forall {a} -> a -> (n : ℕ) -> a ^ (1# + n) -> a ^ n
-  x <$ ε     $> f = f x
-  x <$ _ ◅ n $> f = \y -> x <$ n $> f y
+  _<$_$>_ : forall {a} -> a -> (n : ℕ) -> a ^ (1 + n) -> a ^ n
+  x <$ zero  $> f = f x
+  x <$ suc n $> f = \y -> x <$ n $> f y
hunk ./ApplicationBased.agda 50
-  ⟦_⟧' : Expr -> ℕ ^ 0#
+  ⟦_⟧' : Expr -> ℕ ^ 0
hunk ./ApplicationBased.agda 52
-  ⟦ m ⊖ n ⟧' = ⟦ m ⟧' <$ 0# $> (⟦ n ⟧' <$ 1# $> sub)
+  ⟦ m ⊖ n ⟧' = ⟦ m ⟧' <$ 0 $> (⟦ n ⟧' <$ 1 $> sub)
hunk ./ApplicationBased.agda 60
-    return : ℕ -> Cmd 0#
-    sub    : Cmd 2#
+    return : ℕ -> Cmd 0
+    sub    : Cmd 2
hunk ./ApplicationBased.agda 64
-    cmd  : forall {n} -> Cmd n -> Tree (1# + n)
-    _$$_ : forall {n} -> Tree 1# -> Tree (1# + n) -> Tree n
+    cmd  : forall {n} -> Cmd n -> Tree (1 + n)
+    _$$_ : forall {n} -> Tree 1 -> Tree (1 + n) -> Tree n
hunk ./ApplicationBased.agda 67
-  comp : Expr -> Tree 1#
+  comp : Expr -> Tree 1
hunk ./ApplicationBased.agda 82
-    push : forall {n} -> ℕ -> Cmd n (1# + n)
-    sub  : forall {n} -> Cmd (2# + n) (1# + n)
+    push : forall {n} -> ℕ -> Cmd n (1 + n)
+    sub  : forall {n} -> Cmd (2 + n) (1 + n)
hunk ./ApplicationBased.agda 91
-  comp : forall {m n} -> Tree (1# + m) -> Code (m + n) (1# + n)
+  comp : forall {m n} -> Tree (1 + m) -> Code (m + n) (1 + n)
hunk ./ApplicationBased.agda 97
-  exec ε             s               = s
-  exec (push n ◅ cs) s               = exec cs (n ∷ s)
-  exec (sub    ◅ cs) (↦ n ◅ ↦ m ◅ s) = exec cs (m ∸ n ∷ s)
+  exec ε             s           = s
+  exec (push n ◅ cs) s           = exec cs (n ∷ s)
+  exec (sub    ◅ cs) (n ∷ m ∷ s) = exec cs (m ∸ n ∷ s)
hunk ./ApplicationBased.agda 107
-  Code = Step₃.Code 0# 1#
+  Code = Step₃.Code 0 1
hunk ./ApplicationBased.agda 113
-  exec cs = head (Step₃.exec cs ε)
+  exec cs = head (Step₃.exec cs [])