Module `Logtk.Ind_ty`Source

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.

Sourceval section : Util.Section.t

Sourcetype constructor = private {

cstor_name : ID.t;
cstor_ty : Type.t;
cstor_args : (Type.t * projector) list;

}

Constructor for an inductive type

Sourceand projector = private {

p_id : ID.t;
p_ty : Type.t;
p_index : int;
p_cstor : constructor lazy_t;

}

A projector for a given constructor and argument position

Inductive Types

Sourcetype t = private {

ty_id : ID.t;
ty_vars : Type.t HVar.t list;
ty_pattern : Type.t;
ty_constructors : constructor list;
ty_is_rec : bool lazy_t;
ty_proof : Proof.t;

}

An inductive type, along with its set of constructors

Sourceval pp : t CCFormat.printer

Sourceexception InvalidDecl of string

Sourceexception NotAnInductiveType of ID.t

Sourceexception NotAnInductiveConstructor of ID.t

Source

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

Sourceval as_inductive_ty : ID.t -> t option

Sourceval as_inductive_ty_exn : ID.t -> t

Unsafe version of as_inductive_ty

raises NotAnInductiveType
if the ID is not an inductive type

Sourceval is_inductive_ty : ID.t -> bool

Sourceval 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

Sourceval as_inductive_type_exn : Type.t -> t * Type.t list

Sourceval is_inductive_type : Type.t -> bool

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

Sourceval is_inductive_simple_type : TypedSTerm.t -> bool

Sourceval is_recursive : t -> bool

Sourceval proof : t -> Proof.t

Constructors

Source

val mk_constructor : 
  ID.t ->
  Type.t ->
  (Type.t * (ID.t * Type.t)) list ->
  constructor

Sourceval is_constructor : ID.t -> bool

true if the symbol is an inductive constructor (zero, successor...)

Sourceval as_constructor : ID.t -> (constructor * t) option

if id is a constructor of ity, then as_constructor id returns Some (cstor, ity)

Sourceval as_constructor_exn : ID.t -> constructor * t

Unsafe version of as_constructor

raises NotAnInductiveConstructor
if it fails

Sourceval contains_inductive_types : Term.t -> bool

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

Projectors

Sourceval projector_id : projector -> ID.t

Sourceval projector_ty : projector -> Type.t

Sourceval projector_idx : projector -> int

Sourceval projector_cstor : projector -> constructor

Sourceval as_projector : ID.t -> projector option

package logtk

Module Logtk.Ind_tySource

Inductive Types

Inductive Types

Constructors

Projectors

Module `Logtk.Ind_ty`Source