Mercurial > cpdt > repo

comparison src/DepList.v @ 126:d7aec67f808b

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
More DepList notations
author Adam Chlipala <adamc@hcoop.net>
date Mon, 20 Oct 2008 12:17:39 -0400
parents 8a548a6c7074
children e70fbfc56c46
comparison
equal deleted inserted replaced
125:8a548a6c7074 126:d7aec67f808b
62 match ls with 62 match ls with
63 | nil => Empty_set 63 | nil => Empty_set
64 | x :: ls' => (x = elm) + member ls' 64 | x :: ls' => (x = elm) + member ls'
65 end%type. 65 end%type.
66 66
67 Definition hfirst (x : A) (ls : list A) (pf : x = elm) : member (x :: ls) :=
68 inl _ pf.
69 Definition hnext (x : A) (ls : list A) (m : member ls) : member (x :: ls) :=
70 inr _ m.
71
67 Fixpoint hget (ls : list A) : hlist ls -> member ls -> B elm := 72 Fixpoint hget (ls : list A) : hlist ls -> member ls -> B elm :=
68 match ls return hlist ls -> member ls -> B elm with 73 match ls return hlist ls -> member ls -> B elm with
69 | nil => fun _ idx => match idx with end 74 | nil => fun _ idx => match idx with end
70 | _ :: ls' => fun mls idx => 75 | _ :: ls' => fun mls idx =>
71 match idx with 76 match idx with
86 Implicit Arguments hnil [A B]. 91 Implicit Arguments hnil [A B].
87 Implicit Arguments hcons [A B x ls]. 92 Implicit Arguments hcons [A B x ls].
88 Implicit Arguments hget [A B elm ls]. 93 Implicit Arguments hget [A B elm ls].
89 Implicit Arguments happ [A B ls1 ls2]. 94 Implicit Arguments happ [A B ls1 ls2].
90 95
96 Implicit Arguments hfirst [A elm x ls].
97 Implicit Arguments hnext [A elm x ls].
98
91 Infix ":::" := hcons (right associativity, at level 60). 99 Infix ":::" := hcons (right associativity, at level 60).
92 Infix "+++" := happ (right associativity, at level 60). 100 Infix "+++" := happ (right associativity, at level 60).