# HG changeset patch
# User Adam Chlipala <adamc@hcoop.net>
# Date 1224513860 14400
# Node ID 8a548a6c70748655f2541686fd7edff6a05020b1
# Parent  57eaceb085f6643cdefa4c3b23776e5f9baf5d97
Add ext_eq axiom and DepList notations

diff -r 57eaceb085f6 -r 8a548a6c7074 Makefile
--- a/Makefile	Mon Oct 20 09:11:54 2008 -0400
+++ b/Makefile	Mon Oct 20 10:44:20 2008 -0400
@@ -1,4 +1,4 @@
-MODULES_NODOC := Tactics MoreSpecif DepList
+MODULES_NODOC := Axioms Tactics MoreSpecif DepList
 MODULES_PROSE := Intro
 MODULES_CODE  := StackMachine InductiveTypes Predicates Coinductive Subset \
 	MoreDep DataStruct Equality
diff -r 57eaceb085f6 -r 8a548a6c7074 src/Axioms.v
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Axioms.v	Mon Oct 20 10:44:20 2008 -0400
@@ -0,0 +1,17 @@
+(* Copyright (c) 2008, Adam Chlipala
+ * 
+ * This work is licensed under a
+ * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
+ * Unported License.
+ * The license text is available at:
+ *   http://creativecommons.org/licenses/by-nc-nd/3.0/
+ *)
+
+(* Additional axioms not in the Coq standard library *)
+
+Axiom ext_eq : forall (A : Type) (B : A -> Type)
+  (f g : forall x, B x),
+  (forall x, f x = g x)
+  -> f = g.
+
+Ltac ext_eq := apply ext_eq; intro.
diff -r 57eaceb085f6 -r 8a548a6c7074 src/DepList.v
--- a/src/DepList.v	Mon Oct 20 09:11:54 2008 -0400
+++ b/src/DepList.v	Mon Oct 20 10:44:20 2008 -0400
@@ -52,6 +52,10 @@
       | x :: ls' => B x * hlist ls'
     end%type.
 
+  Definition hnil : hlist nil := tt.
+  Definition hcons (x : A) (ls : list A) (v : B x) (hls : hlist ls) : hlist (x :: ls) :=
+    (v, hls).
+
   Variable elm : A.
 
   Fixpoint member (ls : list A) : Type :=
@@ -71,6 +75,18 @@
           | inr idx' => hget ls' (snd mls) idx'
         end
     end.
+
+  Fixpoint happ (ls1 ls2 : list A) {struct ls1} : hlist ls1 -> hlist ls2 -> hlist (ls1 ++ ls2) :=
+    match ls1 return hlist ls1 -> hlist ls2 -> hlist (ls1 ++ ls2) with
+      | nil => fun _ hls2 => hls2
+      | _ :: _ => fun hls1 hls2 => (fst hls1, happ _ _ (snd hls1) hls2)
+    end.
 End hlist.
 
+Implicit Arguments hnil [A B].
+Implicit Arguments hcons [A B x ls].
 Implicit Arguments hget [A B elm ls].
+Implicit Arguments happ [A B ls1 ls2].
+
+Infix ":::" := hcons (right associativity, at level 60).
+Infix "+++" := happ (right associativity, at level 60).