25 lines
479 B
OCaml
25 lines
479 B
OCaml
type t =
|
|
| 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
|
|
|
|
type precedence =
|
|
| Atomic
|
|
| Negation
|
|
| Conjunction
|
|
| Disjunction
|
|
| Implication
|
|
| Biconditional
|
|
| Quantifier
|
|
|
|
val precedence_of : t -> precedence
|
|
val match_term : Term.t -> t -> t -> Term.match_result
|
|
val occurs : Term.t -> t -> bool
|
|
val to_string : t -> string
|