[Replaced type vectors with type lists.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20080224022258
 + Since I don't need to know the length.
] hunk ./Wand.agda 28
-data TypeVec : ℕ -> Set1 where
-  []  : TypeVec 0
-  _∷_ : forall {n} -> Set -> TypeVec n -> TypeVec (suc n)
+data TypeList : Set1 where
+  []  : TypeList
+  _∷_ : Set -> TypeList -> TypeList
hunk ./Wand.agda 32
-Fun : forall {n} -> TypeVec n -> Set -> Set
+Fun : TypeList -> Set -> Set
hunk ./Wand.agda 36
-_++_ : forall {n₁ n₂} -> TypeVec n₁ -> TypeVec n₂ -> TypeVec (n₁ + n₂)
+_++_ : TypeList -> TypeList -> TypeList
hunk ./Wand.agda 40
-lemma : forall {a n₁ n₂} (ts₁ : TypeVec n₁) {ts₂ : TypeVec n₂} ->
+lemma : forall {a} ts₁ {ts₂} ->
hunk ./Wand.agda 52
-_⟪_⟫_ : forall {a b n} ->
-        (a -> b) -> (ts : TypeVec n) -> Fun ts a -> Fun ts b
+_⟪_⟫_ : forall {a b} ->
+        (a -> b) -> (ts : TypeList) -> Fun ts a -> Fun ts b
hunk ./Wand.agda 57
-_⟪_⟫-cong_ : forall {a b n} {f₁ f₂ : a -> b} ->
+_⟪_⟫-cong_ : forall {a b} {f₁ f₂ : a -> b} ->
hunk ./Wand.agda 59
-             (ts : TypeVec n) {g₁ g₂ : Fun ts a} -> g₁ ≡ g₂ ->
+             (ts : TypeList) {g₁ g₂ : Fun ts a} -> g₁ ≡ g₂ ->
hunk ./Wand.agda 63
-merge : forall {a n₁ n₂} (ts₁ : TypeVec n₁) {ts₂ : TypeVec n₂} ->
+merge : forall {a} ts₁ {ts₂} ->
hunk ./Wand.agda 68
-_⟪_⟫'_ : forall {a b n₁ n₂} {ts₂ : TypeVec n₂} ->
-         (a -> Fun ts₂ b) -> (ts₁ : TypeVec n₁) ->
+_⟪_⟫'_ : forall {a b ts₂} ->
+         (a -> Fun ts₂ b) -> (ts₁ : TypeList) ->
hunk ./Wand.agda 78
--- _⟪_⟫'_ : forall {a b n₁ n₂} {ts₂ : TypeVec n₂} ->
---          (a -> Fun ts₂ b) -> (ts₁ : TypeVec n₁) ->
+-- _⟪_⟫'_ : forall {a b ts₂} ->
+--          (a -> Fun ts₂ b) -> (ts₁ : TypeList) ->
hunk ./Wand.agda 83
-right-assoc : forall {n₁ n₂ a b t}
-              (ts₁ : TypeVec n₁) {ts₂ : TypeVec n₂}
+right-assoc : forall {a b t} ts₁ {ts₂}