module Term_literal: sig .. end
Term literals.
val is_literal : Term.term -> bool
Holds when a term is a variable or the negation of a variable.
val variable : Term.term -> Term.term
variable l is the variable contained in a literal term.
val is_positive : Term.term -> bool
is_positive l holds if the literal term
t is positive.
val literal : Term.term -> Term.term
literal v is the positive literal term with variable
v.
val negation : Term.term -> Term.term
Negation of a term literal.
- Require
is_literal l
- Ensure
is_positive (negation l) = not (is_positive l)
- Ensure
variable (negation l) = variable l
Hosted by the
* web site.
*Other names and brands may be claimed as the property
of others.