A (sidekick-base.Sidekick_base_solver.Th

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

module P : sig ... end