Kind (qed.Qed.Kind)

val of_tau : ('f, 'a) Logic.datatype -> Logic.sort

val of_poly : (int -> Logic.sort) -> ('f, 'a) Logic.datatype -> Logic.sort

val image : Logic.sort -> Logic.sort

val degree_of_tau : ('f, 'a) Logic.datatype -> int

val degree_of_list : ('f, 'a) Logic.datatype list -> int

val degree_of_sig : ('f, 'a) Logic.funtype -> int

val type_params : int -> ('f, 'a) Logic.datatype list

val merge : Logic.sort -> Logic.sort -> Logic.sort

val merge_list : ('a -> Logic.sort) -> Logic.sort -> 'a list -> Logic.sort

val tmap : 
  ('a, 'f) Logic.datatype array ->
  ('a, 'f) Logic.datatype ->
  ('a, 'f) Logic.datatype

val basename : Logic.sort -> string

val pretty : Stdlib.Format.formatter -> Logic.sort -> unit

val pp_tau : 
  (Stdlib.Format.formatter -> int -> unit) ->
  (Stdlib.Format.formatter -> 'f -> unit) ->
  (Stdlib.Format.formatter -> 'a -> unit) ->
  Stdlib.Format.formatter ->
  ('f, 'a) Logic.datatype ->
  unit

val pp_data : 
  (Stdlib.Format.formatter -> 'a -> unit) ->
  (Stdlib.Format.formatter -> 'b -> unit) ->
  Stdlib.Format.formatter ->
  'a ->
  'b list ->
  unit

val pp_record : 
  (Stdlib.Format.formatter -> 'f -> unit) ->
  (Stdlib.Format.formatter -> 'b -> unit) ->
  Stdlib.Format.formatter ->
  ?opened:bool ->
  ('f * 'b) list ->
  unit

val eq_tau : 
  ('f -> 'f -> bool) ->
  ('a -> 'a -> bool) ->
  ('f, 'a) Logic.datatype ->
  ('f, 'a) Logic.datatype ->
  bool

val compare_tau : 
  ('f -> 'f -> int) ->
  ('a -> 'a -> int) ->
  ('f, 'a) Logic.datatype ->
  ('f, 'a) Logic.datatype ->
  int

module MakeTau
  (F : Logic.Field)
  (A : Logic.Data) : 
  Logic.Data with type t = (F.t, A.t) Logic.datatype