module Term_constant: sig .. end
Predefined Constants.
Boolean Constants
val truth : Term.term
Logical true.
val falsity : Term.term
Logical false.
val negation : Term.term
Logical negation.
val conjunction : Term.term
Logical conjunction.
val disjunction : Term.term
Logical disjunction.
val equivalence : Term.term
Logical equivalence.
val difference : Term.term
Exclusive or.
val implication : Term.term
Logical implication.
val conditional : Term.term
Logical if-then-else.
Updatable function constants
val k : Term.term
Constant function constructor.
val update : Term.term
Function update operator.
val mk_array : Term.term
Array constants
Constant array.
val select : Term.term
Array select.
val store : Term.term
Array store.
Arithmetic Constants
val unary_minus : Term.term
Arithmetic unary minus.
val plus : Term.term
Arithmetic addition.
val minus : Term.term
Arithmetic subtraction.
val times : Term.term
Arithmetic multiplication.
val divide : Term.term
Arithmetic division.
val less : Term.term
Less-than relation.
val less_or_equal : Term.term
Less-than-or-equal relation.
val greater : Term.term
Greater-than relation.
val greater_or_equal : Term.term
Greater-than-or-equal relation.
Polymorphic Constants
val equality : Term.term
Equality
val ite : Term.term
If-then-else
Predicates
val is_boolean_constant : Term.term -> bool
val is_logical_constant : Term.term -> bool
Hosted by the
* web site.
*Other names and brands may be claimed as the property
of others.