Module `Mc2_unin_sort`

Uninterpreted Functions and Types

val k_decl_sort : (Mc2_core.ID.t -> int -> unit) Mc2_core.Service.Key.t: Declare a uninterpreted sort

val k_make : (Mc2_core.ID.t -> Mc2_core.Type.t list -> Mc2_core.Type.t) Mc2_core.Service.Key.t: Build an instance of an uninterpreted sort

val k_eq : (Mc2_core.term -> Mc2_core.term -> Mc2_core.term) Mc2_core.Service.Key.t: Equality between terms of unintepreted sorts

val plugin : Mc2_core.Plugin.Factory.t