package alt-ergo-lib

The type of semantic elements literals.

The type of syntaxic or semantic literals.

Create a new literal given its view.

Extract a view from a literal (for pattern-matching).

Pretty-printer for literals.

Hash function for literals.

Equality of literals. Note that this does not try to look into the semantic content of syntaxic literals: x = y as a term and x = y as a semantic literal (where x and y are semantic values) are distinct.

Comparison function over literals. The order is unspecified.

neg t is the boolean negation of t.

normal_form l returns the normal form of l. The normal form of l is a pair l', is_neg such that:

• l' is neg l if is_neg is true
• l' is l if is_neg is false
• normal_form l' is l', false

normal_form l returns the normal form of l. The normal form of l is a pair l', is_neg such that:

• l' is neg l if is_neg is true
• l' is l if is_neg is false
• normal_form l' is l', false

is_ground l is always true if l is a semantic literal, and otherwise is true iff the syntaxic literal is ground (does not contain free variables nor free type variables).

Hash tables over literals.

Sets of literals.

Maps over literals.