src/ZF/ex/ListN.thy
author clasohm
Sat Dec 09 13:36:11 1995 +0100 (1995-12-09 ago)
changeset 1401 0c439768f45c
parent 515 abcc438e7c27
child 1478 2b8c2a7547ab
permissions -rw-r--r--
removed quotes from consts and syntax sections
lcp@515
     1
(*  Title: 	ZF/ex/ListN
lcp@515
     2
    ID:         $Id$
lcp@515
     3
    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
lcp@515
     4
    Copyright   1994  University of Cambridge
lcp@515
     5
lcp@515
     6
Inductive definition of lists of n elements
lcp@515
     7
lcp@515
     8
See Ch. Paulin-Mohring, Inductive Definitions in the System Coq.
lcp@515
     9
Research Report 92-49, LIP, ENS Lyon.  Dec 1992.
lcp@515
    10
*)
lcp@515
    11
lcp@515
    12
ListN = List +
clasohm@1401
    13
consts	listn ::i=>i
lcp@515
    14
inductive
lcp@515
    15
  domains   "listn(A)" <= "nat*list(A)"
lcp@515
    16
  intrs
lcp@515
    17
    NilI  "<0,Nil> : listn(A)"
lcp@515
    18
    ConsI "[| a: A;  <n,l> : listn(A) |] ==> <succ(n), Cons(a,l)> : listn(A)"
lcp@515
    19
  type_intrs "nat_typechecks @ list.intrs"
lcp@515
    20
end