Module Term_constant

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
val ite : Term.term


val is_boolean_constant : Term.term -> bool
val is_logical_constant : Term.term -> bool

Hosted by the Logo* web site.
*Other names and brands may be claimed as the property of others.