logtk

Core types and algorithms for logic
Legend:
Library
Module
Module type
Parameter
Class
Class type
Library logtk
Module Logtk . Builtin . Tag
type t =
| T_lia(*

integer arith

*)
| T_lra(*

rational arith

*)
| T_ho(*

higher order

*)
| T_live_cnf(*

live_cnf

*)
| T_ho_norm(*

higher-order normalization

*)
| T_dont_increase_depth(*

don't increase depth

*)
| T_ext(*

extensionality

*)
| T_ind(*

induction

*)
| T_data(*

datatypes

*)
| T_distinct(*

distinct constants

*)
| T_ac of ID.t(*

AC symbol

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