[Made the code a bit more tidy.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20091127194434
 Ignore-this: 6e4a554add27d8b6d2b68a4683a43aa0
] hunk ./CompositionBased.agda 11
-open import Data.Vec.N-ary
hunk ./CompositionBased.agda 53
-                                          (proof (eval e₂))
-                                          (proof (eval e₁)) ⟩
+                                            (proof (eval e₂))
+                                            (proof (eval e₁)) ⟩
hunk ./CompositionBased.agda 76
-                                              (proof (eval e₁ (sub ⊙ f))) ⟩
+                                               (proof (eval e₁ (sub ⊙ f))) ⟩
hunk ./ReverseComposition.agda 49
--- Heterogeneous equality.
+------------------------------------------------------------------------
+-- A specialised variant of _⇨_
+
+_↑_ : Set → ℕ → Set
+A ↑ n = List.replicate n A ⇨ A
+
+-- Applies the function to a vector of arguments.
+
+app : ∀ {A n} → A ↑ n → Vec A n → A
+app x []       = ! x
+app f (x ∷ xs) = app (f · x) xs
+
+------------------------------------------------------------------------
+-- Heterogeneous equality
hunk ./ReverseComposition.agda 113
-------------------------------------------------------------------------
--- A specialised variant of _⇨_
-
-_↑_ : Set → ℕ → Set
-A ↑ n = List.replicate n A ⇨ A
-
--- Applies the function to a vector of arguments.
-
-app : ∀ {A n} → A ↑ n → Vec A n → A
-app x []       = ! x
-app f (x ∷ xs) = app (f · x) xs
-