module Ind_ty: sig
.. end
Inductive Types
val section : Util.Section.t
type
constructor = {
}
Constructor for an inductive type
Inductive Types
type
t = private {
}
An inductive type, along with its set of constructors
exception InvalidDecl of string
exception NotAnInductiveType of ID.t
exception NotAnInductiveConstructor of ID.t
val declare_ty : ID.t -> ty_vars:Type.t HVar.t list -> constructor list -> t
Declare the given inductive type.
Raises InvalidDecl
if the type is already declared, or the list
of constructors is empty
val as_inductive_ty : ID.t -> t option
val as_inductive_ty_exn : ID.t -> t
val is_inductive_ty : ID.t -> bool
val as_inductive_type : Type.t -> t option
val is_inductive_type : Type.t -> bool
is_inductive_type ty
holds iff
ty
is an instance of some
registered type (registered with
Ind_ty.declare_ty
).
Constructors
val is_constructor : ID.t -> bool
true if the symbol is an inductive constructor (zero, successor...)
val as_constructor : ID.t -> (constructor * t) option
if id
is a constructor of ity
, then as_constructor id
returns Some (cstor, ity)
val as_constructor_exn : ID.t -> constructor * t
val contains_inductive_types : FOTerm.t -> bool
true
iff the term contains at least one subterm with
an inductive type
Constants with Inductive Type
val is_inductive_constant : ID.t -> bool
An ID whose type is inductive; nothing more
val declare_inductive_constant : ID.t -> unit
val scan_for_constant : ID.t -> Type.t -> unit
Scan Declarations
val scan_stmt : ('a, 'b, Type.t, 'c) Statement.t -> unit
Exceptions used to store information in IDs
exception Payload_ind_type of t
exception Payload_ind_cstor of constructor * t
exception Payload_ind_constant
exception Payload_ind_projector of ID.t