Module Builtin.Tag

Each tag describes an extension of FO logic

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
val pp : t CCFormat.printer