Mercurial > cpdt > repo

comparison src/DepList.v @ 215:f8bcd33bdd91

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Port DataStruct
author Adam Chlipala <adamc@hcoop.net>
date Wed, 11 Nov 2009 14:00:04 -0500
parents f6293ba66559
children d1464997078d
comparison
equal deleted inserted replaced
214:768889c969e9 215:f8bcd33bdd91
29 Definition hd n (ls : ilist (S n)) : A := fst ls. 29 Definition hd n (ls : ilist (S n)) : A := fst ls.
30 Definition tl n (ls : ilist (S n)) : ilist n := snd ls. 30 Definition tl n (ls : ilist (S n)) : ilist n := snd ls.
31 31
32 Implicit Arguments icons [n]. 32 Implicit Arguments icons [n].
33 33
34 Fixpoint index (n : nat) : Type := 34 Fixpoint fin (n : nat) : Type :=
35 match n with 35 match n with
36 | O => Empty_set 36 | O => Empty_set
37 | S n' => option (index n') 37 | S n' => option (fin n')
38 end. 38 end.
39 39
40 Fixpoint get (n : nat) : ilist n -> index n -> A := 40 Fixpoint get (n : nat) : ilist n -> fin n -> A :=
41 match n return ilist n -> index n -> A with 41 match n return ilist n -> fin n -> A with
42 | O => fun _ idx => match idx with end 42 | O => fun _ idx => match idx with end
43 | S n' => fun ls idx => 43 | S n' => fun ls idx =>
44 match idx with 44 match idx with
45 | None => fst ls 45 | None => fst ls
46 | Some idx' => get n' (snd ls) idx' 46 | Some idx' => get n' (snd ls) idx'