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