Mercurial > cpdt > repo

comparison src/DepList.v @ 123:9ccd215e5112

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
ext_eq
author Adam Chlipala <adamc@hcoop.net>
date Sat, 18 Oct 2008 17:36:08 -0400
parents 2f97c8177172
children 8a548a6c7074
comparison
equal deleted inserted replaced
122:7cbf0376702f 123:9ccd215e5112
13 13
14 Set Implicit Arguments. 14 Set Implicit Arguments.
15 15
16 16
17 Section ilist. 17 Section ilist.
18 Variable A : Set. 18 Variable A : Type.
19 19
20 Fixpoint ilist (n : nat) : Set := 20 Fixpoint ilist (n : nat) : Type :=
21 match n with 21 match n with
22 | O => unit 22 | O => unit
23 | S n' => A * ilist n' 23 | S n' => A * ilist n'
24 end%type. 24 end%type.
25 25
26 Fixpoint index (n : nat) : Set := 26 Fixpoint index (n : nat) : Type :=
27 match n with 27 match n with
28 | O => Empty_set 28 | O => Empty_set
29 | S n' => option (index n') 29 | S n' => option (index n')
30 end. 30 end.
31 31