Module Logtk.Ind_ty

Inductive Types

An inductive datatype, defined by a list of constructors (and associated projectors that are defined as partial functions). Inductive types can be mutually recursive.

val section : Util.Section.t
type constructor = private {
  1. cstor_name : ID.t;
  2. cstor_ty : Type.t;
  3. cstor_args : (Type.t * projector) list;
}

Constructor for an inductive type

and projector = private {
  1. p_id : ID.t;
  2. p_ty : Type.t;
  3. p_index : int;
  4. p_cstor : constructor lazy_t;
}

A projector for a given constructor and argument position

Inductive Types
type t = private {
  1. ty_id : ID.t;
  2. ty_vars : Type.t HVar.t list;
  3. ty_pattern : Type.t;
  4. ty_constructors : constructor list;
  5. ty_is_rec : bool lazy_t;
  6. ty_proof : Proof.t;
}

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 -> proof:Proof.t -> 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

Unsafe version of as_inductive_ty

val is_inductive_ty : ID.t -> bool
val as_inductive_type : Type.t -> (t * Type.t list) option

as_inductive_ty (list int) will return list, [int] as an inductive type applied to some arguments

val as_inductive_type_exn : Type.t -> t * Type.t list
val is_inductive_type : Type.t -> bool

is_inductive_type ty holds iff ty is an instance of some registered type (registered with declare_ty).

val is_inductive_simple_type : TypedSTerm.t -> bool
val is_recursive : t -> bool
val proof : t -> Proof.t
Constructors
val mk_constructor : ID.t -> Type.t -> (Type.t * (ID.t * Type.t)) list -> constructor
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

Unsafe version of as_constructor

val contains_inductive_types : Term.t -> bool

true iff the term contains at least one subterm with an inductive type

Projectors
val projector_id : projector -> ID.t
val projector_ty : projector -> Type.t
val projector_idx : projector -> int
val projector_cstor : projector -> constructor
val as_projector : ID.t -> projector option