module EnumTypes:`sig`

..`end`

type`term =`

`Logtk.Term.t`

An Enum Type is a possibly parametrized type

`c : type -> type -> ... -> type`

with an exhaustiveness axiom
```
forall a1....an:type,
forall x:(c a1...an),
x = t_1 or x = t_2 or ... or x = t_m
```

where the `t_i`

are non-variable terms that contain
only `x`

as a variable.
This calculus is designed to remove the axiom (which is very prolific in superposition) and do its job more efficiently.

Inductive types (algebraic types) belong to this category of types, and have additional axioms that are dealt with elsewhere.

We require that the type is as general as possible: either
a constant, or a polymorphic type that has only type variables as
arguments. Enum types for things like `list(int)`

would be dangerous
because if we remove the axiom, because instantiation is a
simplification, we won't deal properly with `list(rat)`

(no unification
whatsoever)

The rules are:

instantiation of variables:

C`x`

where x:tau unshielded enum(tau, x in t1....tm)
-----------------------------------------------------------
C`t_1`

or ... or C`tm`

specialization of exhaustiveness for f:

f : a1 -> ... -> ak -> tau enum(tau, x in t1....tm)
------------------------------------------------------------
forall x1:a1, ... xk:ak,
f(x1...xk)=t1\sigma or .... or f(x1...xk) = tm\sigma
where sigma =

`exception Error of ``string`

module type S =`sig`

..`end`

module Make:

`val extension : ``Extensions.t`