kernel/inductive.mli


1
2
3
4
5
6
7
8
9
10
11
12

(* $Id$ *)

open Names

type mind_entry

type mutual_inductive_body

type mutual_inductive_entry = section_path * mutual_inductive_body

val mind_type_finite : mutual_inductive_body -> int -> bool