[Improved the documentation.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20091104235649
 Ignore-this: 45fde22a7b85f3c016b2f255b431ffda
] hunk ./ApplicationBased.agda 23
--- since subtraction is not commutative, so the arguments cannot be
+-- because subtraction is not commutative, so the arguments cannot be
hunk ./ApplicationBased.agda 30
--- Its semantics.
+-- The semantics of the language.
hunk ./ApplicationBased.agda 41
+  -- The type A ^ n represents functions from stacks with n elements
+  -- to a single result. The first function argument is the top of the
+  -- stack.
+
hunk ./ApplicationBased.agda 55
+  -- x <$ n $> f puts x at the bottom of the stack given to f:
+  --
+  --   x <$ n $> f = λ y₁ … y_n → f y₁ … y_n x
+
hunk ./ApplicationBased.agda 120
+  -- app interprets functions of type ℕ ^ m:
+  --
+  --   app m f (x₁ ∷ … ∷ x_m ∷ ys) = f x_m … x₁ ∷ ys
+