Module Qed.Kind

Logic Types Utilities

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