Mercurial > cpdt > repo

comparison src/DepList.v @ 125:8a548a6c7074

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Add ext_eq axiom and DepList notations
author Adam Chlipala <adamc@hcoop.net>
date Mon, 20 Oct 2008 10:44:20 -0400
parents 9ccd215e5112
children d7aec67f808b
comparison
equal deleted inserted replaced
124:57eaceb085f6 125:8a548a6c7074
50 match ls with 50 match ls with
51 | nil => unit 51 | nil => unit
52 | x :: ls' => B x * hlist ls' 52 | x :: ls' => B x * hlist ls'
53 end%type. 53 end%type.
54 54
55 Definition hnil : hlist nil := tt.
56 Definition hcons (x : A) (ls : list A) (v : B x) (hls : hlist ls) : hlist (x :: ls) :=
57 (v, hls).
58
55 Variable elm : A. 59 Variable elm : A.
56 60
57 Fixpoint member (ls : list A) : Type := 61 Fixpoint member (ls : list A) : Type :=
58 match ls with 62 match ls with
59 | nil => Empty_set 63 | nil => Empty_set
69 | refl_equal => fst mls 73 | refl_equal => fst mls
70 end 74 end
71 | inr idx' => hget ls' (snd mls) idx' 75 | inr idx' => hget ls' (snd mls) idx'
72 end 76 end
73 end. 77 end.
78
79 Fixpoint happ (ls1 ls2 : list A) {struct ls1} : hlist ls1 -> hlist ls2 -> hlist (ls1 ++ ls2) :=
80 match ls1 return hlist ls1 -> hlist ls2 -> hlist (ls1 ++ ls2) with
81 | nil => fun _ hls2 => hls2
82 | _ :: _ => fun hls1 hls2 => (fst hls1, happ _ _ (snd hls1) hls2)
83 end.
74 End hlist. 84 End hlist.
75 85
86 Implicit Arguments hnil [A B].
87 Implicit Arguments hcons [A B x ls].
76 Implicit Arguments hget [A B elm ls]. 88 Implicit Arguments hget [A B elm ls].
89 Implicit Arguments happ [A B ls1 ls2].
90
91 Infix ":::" := hcons (right associativity, at level 60).
92 Infix "+++" := happ (right associativity, at level 60).