changeset 126:d7aec67f808b

More DepList notations
author Adam Chlipala <adamc@hcoop.net>
date Mon, 20 Oct 2008 12:17:39 -0400
parents 8a548a6c7074
children 0bfc75502498
files src/DepList.v
diffstat 1 files changed, 8 insertions(+), 0 deletions(-) [+]
line wrap: on
line diff
--- 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).