equal
deleted
inserted
replaced
1 (* Title: ZF/ex/ListN |
|
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 Copyright 1994 University of Cambridge |
|
5 |
|
6 Inductive definition of lists of n elements |
|
7 |
|
8 See Ch. Paulin-Mohring, Inductive Definitions in the System Coq. |
|
9 Research Report 92-49, LIP, ENS Lyon. Dec 1992. |
|
10 *) |
|
11 |
|
12 ListN = Main + |
|
13 |
|
14 consts listn ::i=>i |
|
15 inductive |
|
16 domains "listn(A)" <= "nat*list(A)" |
|
17 intrs |
|
18 NilI "<0,Nil> \\<in> listn(A)" |
|
19 ConsI "[| a \\<in> A; <n,l> \\<in> listn(A) |] ==> <succ(n), Cons(a,l)> \\<in> listn(A)" |
|
20 type_intrs "nat_typechecks @ list.intrs" |
|
21 |
|
22 end |
|