equal
deleted
inserted
replaced
7 |
7 |
8 See Ch. Paulin-Mohring, Inductive Definitions in the System Coq. |
8 See Ch. Paulin-Mohring, Inductive Definitions in the System Coq. |
9 Research Report 92-49, LIP, ENS Lyon. Dec 1992. |
9 Research Report 92-49, LIP, ENS Lyon. Dec 1992. |
10 *) |
10 *) |
11 |
11 |
12 ListN = List + |
12 ListN = Main + |
|
13 |
13 consts listn ::i=>i |
14 consts listn ::i=>i |
14 inductive |
15 inductive |
15 domains "listn(A)" <= "nat*list(A)" |
16 domains "listn(A)" <= "nat*list(A)" |
16 intrs |
17 intrs |
17 NilI "<0,Nil> \\<in> listn(A)" |
18 NilI "<0,Nil> \\<in> listn(A)" |
18 ConsI "[| a \\<in> A; <n,l> \\<in> listn(A) |] ==> <succ(n), Cons(a,l)> \\<in> listn(A)" |
19 ConsI "[| a \\<in> A; <n,l> \\<in> listn(A) |] ==> <succ(n), Cons(a,l)> \\<in> listn(A)" |
19 type_intrs "nat_typechecks @ list.intrs" |
20 type_intrs "nat_typechecks @ list.intrs" |
|
21 |
20 end |
22 end |