2024-08-29 22:55:09 -07:00
|
|
|
type t =
|
2024-08-30 00:26:16 -07:00
|
|
|
| Relation of string * Term.t list
|
|
|
|
|
| Equal of Term.t * Term.t
|
|
|
|
|
| Bottom
|
|
|
|
|
| Neg of t
|
|
|
|
|
| Conj of t * t
|
|
|
|
|
| Disj of t * t
|
|
|
|
|
| Impl of t * t
|
|
|
|
|
| Iff of t * t
|
|
|
|
|
| Forall of t
|
|
|
|
|
| Exists of t
|
2024-08-30 11:43:13 -07:00
|
|
|
|
2024-09-02 21:33:18 -07:00
|
|
|
type precedence =
|
|
|
|
|
| Atomic
|
|
|
|
|
| Negation
|
|
|
|
|
| Conjunction
|
|
|
|
|
| Disjunction
|
|
|
|
|
| Implication
|
|
|
|
|
| Biconditional
|
|
|
|
|
| Quantifier
|
|
|
|
|
|
|
|
|
|
val precedence_of : t -> precedence
|
2024-08-30 11:43:13 -07:00
|
|
|
val match_term : Term.t -> t -> t -> Term.match_result
|
|
|
|
|
val occurs : Term.t -> t -> bool
|
2024-09-01 12:35:24 -07:00
|
|
|
val to_string : t -> string
|
