src/ZF/ex/ListN.thy
author clasohm
Sat Dec 09 13:36:11 1995 +0100 (1995-12-09)
changeset 1401 0c439768f45c
parent 515 abcc438e7c27
child 1478 2b8c2a7547ab
permissions -rw-r--r--
removed quotes from consts and syntax sections
     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 = List +
    13 consts	listn ::i=>i
    14 inductive
    15   domains   "listn(A)" <= "nat*list(A)"
    16   intrs
    17     NilI  "<0,Nil> : listn(A)"
    18     ConsI "[| a: A;  <n,l> : listn(A) |] ==> <succ(n), Cons(a,l)> : listn(A)"
    19   type_intrs "nat_typechecks @ list.intrs"
    20 end