package logtk

  1. Overview
  2. Docs
package logtk
Legend:
Library
Module
Module type
Parameter
Class
Class type

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
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct