logtk

Core types and algorithms for logic
IN THIS PACKAGE
Module Logtk . Builtin . Tag
type t =
| T_lia(*

integer arith

*)
| T_lra(*

rational arith

*)
| T_ho(*

higher order

*)
| T_ext(*

extensionality

*)
| T_ind(*

induction

*)
| T_data(*

datatypes

*)
| T_distinct(*

distinct constants

*)
| T_ac of ID.t(*

AC symbol

*)
val compare : t -> t -> int