src/ZF/ex/ListN.thy

+(*  Title: 	ZF/ex/ListN
+    ID:         $Id$
+    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1994  University of Cambridge
+
+Inductive definition of lists of n elements
+
+See Ch. Paulin-Mohring, Inductive Definitions in the System Coq.
+Research Report 92-49, LIP, ENS Lyon.  Dec 1992.
+*)
+
+ListN = List +
+consts	listn ::"i=>i"
+inductive
+  domains   "listn(A)" <= "nat*list(A)"
+  intrs
+    NilI  "<0,Nil> : listn(A)"
+    ConsI "[| a: A;  <n,l> : listn(A) |] ==> <succ(n), Cons(a,l)> : listn(A)"
+  type_intrs "nat_typechecks @ list.intrs"
+end