Module `Th_data.A`

module S : sig ... end

module Cstor : sig ... end

val as_datatype : S.T.Ty.t -> (Cstor.t Iter.t, S.T.Ty.t) Sidekick_th_data.data_ty_view
val view_as_data : S.T.Term.t -> (Cstor.t, S.T.Term.t) Sidekick_th_data.data_view
val mk_cstor : S.T.Term.store -> Cstor.t -> S.T.Term.t Sidekick_util.IArray.t -> S.T.Term.t
val mk_is_a : S.T.Term.store -> Cstor.t -> S.T.Term.t -> S.T.Term.t
val mk_sel : S.T.Term.store -> Cstor.t -> int -> S.T.Term.t -> S.T.Term.t
val mk_eq : S.T.Term.store -> S.T.Term.t -> S.T.Term.t -> S.T.Term.t
val ty_is_finite : S.T.Ty.t -> bool
val ty_set_is_finite : S.T.Ty.t -> bool -> unit
val lemma_isa_split : S.Lit.t Iter.t -> S.proof -> unit
val lemma_isa_disj : S.Lit.t Iter.t -> S.proof -> unit
val lemma_cstor_inj : S.Lit.t Iter.t -> S.proof -> unit