Mercurial > cpdt > repo

comparison src/DepList.v @ 114:2f97c8177172

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
DepList
author Adam Chlipala <adamc@hcoop.net>
date Tue, 14 Oct 2008 14:49:51 -0400
parents
children 9ccd215e5112
comparison
equal deleted inserted replaced
113:ccab8a30c05e 114:2f97c8177172
1 (* Copyright (c) 2008, Adam Chlipala
2 *
3 * This work is licensed under a
4 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
5 * Unported License.
6 * The license text is available at:
7 * http://creativecommons.org/licenses/by-nc-nd/3.0/
8 *)
9
10 (* Dependent list types presented in Chapter 8 *)
11
12 Require Import List.
13
14 Set Implicit Arguments.
15
16
17 Section ilist.
18 Variable A : Set.
19
20 Fixpoint ilist (n : nat) : Set :=
21 match n with
22 | O => unit
23 | S n' => A * ilist n'
24 end%type.
25
26 Fixpoint index (n : nat) : Set :=
27 match n with
28 | O => Empty_set
29 | S n' => option (index n')
30 end.
31
32 Fixpoint get (n : nat) : ilist n -> index n -> A :=
33 match n return ilist n -> index n -> A with
34 | O => fun _ idx => match idx with end
35 | S n' => fun ls idx =>
36 match idx with
37 | None => fst ls
38 | Some idx' => get n' (snd ls) idx'
39 end
40 end.
41 End ilist.
42
43 Implicit Arguments get [A n].
44
45 Section hlist.
46 Variable A : Type.
47 Variable B : A -> Type.
48
49 Fixpoint hlist (ls : list A) : Type :=
50 match ls with
51 | nil => unit
52 | x :: ls' => B x * hlist ls'
53 end%type.
54
55 Variable elm : A.
56
57 Fixpoint member (ls : list A) : Type :=
58 match ls with
59 | nil => Empty_set
60 | x :: ls' => (x = elm) + member ls'
61 end%type.
62
63 Fixpoint hget (ls : list A) : hlist ls -> member ls -> B elm :=
64 match ls return hlist ls -> member ls -> B elm with
65 | nil => fun _ idx => match idx with end
66 | _ :: ls' => fun mls idx =>
67 match idx with
68 | inl pf => match pf with
69 | refl_equal => fst mls
70 end
71 | inr idx' => hget ls' (snd mls) idx'
72 end
73 end.
74 End hlist.
75
76 Implicit Arguments hget [A B elm ls].