Module `Auto_ind_decl`

This file is about the automatic generation of schemes about decidable equality,

author: Vincent Siles

Oct 2007

Build boolean equality of a block of mutual inductive types

exception EqNotFound of Names.inductive * Names.inductive
exception EqUnknown of string
exception UndefinedCst of string
exception InductiveWithProduct
exception InductiveWithSort
exception ParameterWithoutEquality of Names.GlobRef.t
exception NonSingletonProp of Names.inductive
exception DecidabilityMutualNotSupported
exception NoDecidabilityCoInductive
exception ConstructorWithNonParametricInductiveType of Names.inductive
exception DecidabilityIndicesNotSupported

val beq_scheme_kind : Ind_tables.mutual Ind_tables.scheme_kind
val build_beq_scheme : Ind_tables.mutual_scheme_object_function

Build equivalence between boolean equality and Leibniz equality

val lb_scheme_kind : Ind_tables.mutual Ind_tables.scheme_kind
val make_lb_scheme : Ind_tables.mutual_scheme_object_function
val bl_scheme_kind : Ind_tables.mutual Ind_tables.scheme_kind
val make_bl_scheme : Ind_tables.mutual_scheme_object_function

Build decidability of equality

val eq_dec_scheme_kind : Ind_tables.mutual Ind_tables.scheme_kind
val make_eq_decidability : Ind_tables.mutual_scheme_object_function