# HG changeset patch
# User Adam Chlipala <adamc@hcoop.net>
# Date 1224519459 14400
# Node ID d7aec67f808b5706ac5f472f5a16c86032f3e197
# Parent  8a548a6c70748655f2541686fd7edff6a05020b1
More DepList notations

diff -r 8a548a6c7074 -r d7aec67f808b src/DepList.v
--- a/src/DepList.v	Mon Oct 20 10:44:20 2008 -0400
+++ b/src/DepList.v	Mon Oct 20 12:17:39 2008 -0400
@@ -64,6 +64,11 @@
       | x :: ls' => (x = elm) + member ls'
     end%type.
 
+  Definition hfirst (x : A) (ls : list A) (pf : x = elm) : member (x :: ls) :=
+    inl _ pf.
+  Definition hnext (x : A) (ls : list A) (m : member ls) : member (x :: ls) :=
+    inr _ m.
+
   Fixpoint hget (ls : list A) : hlist ls -> member ls -> B elm :=
     match ls return hlist ls -> member ls -> B elm with
       | nil => fun _ idx => match idx with end
@@ -88,5 +93,8 @@
 Implicit Arguments hget [A B elm ls].
 Implicit Arguments happ [A B ls1 ls2].
 
+Implicit Arguments hfirst [A elm x ls].
+Implicit Arguments hnext [A elm x ls].
+
 Infix ":::" := hcons (right associativity, at level 60).
 Infix "+++" := happ (right associativity, at level 60).