package logtk

  1. Overview
  2. Docs
package logtk
Legend:
Library
Module
Module type
Parameter
Class
Class type

Each tag describes an extension of FO logic

type t =
  1. | T_lia
    (*

    integer arith

    *)
  2. | T_lra
    (*

    rational arith

    *)
  3. | T_ho
    (*

    higher order

    *)
  4. | T_live_cnf
    (*

    live_cnf

    *)
  5. | T_ho_norm
    (*

    higher-order normalization

    *)
  6. | T_dont_increase_depth
    (*

    don't increase depth

    *)
  7. | T_ext
    (*

    extensionality

    *)
  8. | T_ind
    (*

    induction

    *)
  9. | T_data
    (*

    datatypes

    *)
  10. | T_distinct
    (*

    distinct constants

    *)
  11. | T_ac of ID.t
    (*

    AC symbol

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