# assoc "list" (!inductive_type_store);;
val it : int * thm * thm =
(2, |- !P. P [] /\ (!a0 a1. P a1 ==> P (CONS a0 a1)) ==> (!x. P x),
|- !NIL' CONS'.
?fn. fn [] = NIL' /\
(!a0 a1. fn (CONS a0 a1) = CONS' a0 a1 (fn a1)))
while the following shows that there is an entry for the Boolean
type, for the sake of regularity, even though it is not normally considered an
inductive type:
# assoc "bool" (!inductive_type_store);;
val it : int * thm * thm =
(2, |- !P. P F /\ P T ==> (!x. P x), |- !a b. ?f. f F = a /\ f T = b)