Index of values

(&&) [Rel]
g0 && g1 is a goal succeeds if both g0 and g1 succeed.
(=) [Rel]
t0 = t1 is a goal that succeeds iff there is a unifier for t0 and t1.
(||) [Rel]
g0 || g1 is a goal that succeeds if either g0 or g1 succeeds.

app [Rel]
app d t ret is the application of term t interpreted in domain d to the function returned by ret.
append [Rel_list.Make]
append l0 l1 l succeeds if l1 appended to l0 is l.

bool [Rel.Dom]
bool is a domain for bool values.
bool [Rel]
bool b is const Dom.bool b.

cons [Rel_list.Make]
cons x xs is the list x :: xs.
const [Rel]
const dom v is a term for the constant v in domain dom.

delay [Rel]
delay gazy sees the lazy goal gazy as a goal.
dom [Rel_list.Make]
dom [Rel_list.EL]

empty [Rel_list.Make]
empty is the empty list.
empty [Rel.Seq]
empty is the empty sequence.
equal [Rel.Dom.V]
equal v v' is true iff v and v' are equal.
equal [Rel.Dom]
equal d0 d1 is true iff d0 and d1 are the same domain.
equal_value [Rel.Dom]
equal_value d is d's value equality function.

fail [Rel]
fail is a goal that always fails.
find [Rel.Value]
find v is v's value, if any.
float [Rel.Dom]
float is a domain for float values.
float [Rel]
float f is const Dom.float f.
fresh [Rel]
fresh f is the goal f v with v a fresh logical variable.

get [Rel.Value]
get v is like Rel.Value.find but
get1 [Rel.Value]
get2 [Rel.Value]
get3 [Rel.Value]
get4 [Rel.Value]
get5 [Rel.Value]
get6 [Rel.Value]
get_head [Rel.Seq]
get_head s is like Rel.Seq.head but

hd [Rel_list.Make]
hd l x succeeds if x is the head of l.
head [Rel.Seq]
head s is s's head (if any).

int [Rel.Dom]
int is a domain for int values.
int [Rel]
int i is const i
is_empty [Rel_list.Make]
is_empty l is Rel.(empty = l).
is_empty [Rel.Seq]
is_empty s is true iff s is Rel.Seq.empty.

list [Rel.Dom]
list el is a domain for lists of type 'a.

name [Rel.Value]
name v is v's name.
name [Rel.Dom]
name d is d's name.

of_type [Rel.Dom]
of_type m is a domain from the module m.

pair [Rel.Dom]
pair fst snd is a domain for pairs with first projection fst and second projection snd.
pair [Rel]
pair dom fst snd is a pair for fst and snd in dom.
pp [Rel.Value]
pp ppf v prints, if it exists, v's value using the value's domain pretty-printer.
pp [Rel.Dom.V]
pp ppf v prints an unspecified representation of v on ppf.
pp [Rel.Dom]
pp ppf d prints d's on ppf.
pp_term [Rel]
pp_term ppf t prints an unspecified representation of t on ppf.
pp_value [Rel.Dom]
pp_value d is d's value pretty-printer.
pure [Rel]
pure f is the application that yields f itself.

query [Rel]
query ~name r introduces a logical query variable in r's query and binds its value in the state reyifing function.

reifier [Rel]
reifier q f reifies the query q with reifying function f.
ret [Rel]
ret d app is a term that interprets the application app in domain d and returns a term representing the function application.
rev [Rel_list.Make]
rev l r succeeds if r is the reverse list of l.
run [Rel]
run r is the sequence of states reified by r's reifying function and obtained by running r's query on the empty state.

string [Rel.Dom]
string is a domain for string values.
string [Rel]
string s is const Dom.string s.
succeed [Rel]
succeed is a goal that always succeeds.
success [Rel]
success g is true iff g succeeds on the empty state.

tail [Rel.Seq]
tail s is s's tail.
term [Rel.Value]
term v is v's defining term.
tl [Rel_list.Make]
tl l xs succeeds if xs is the tail of l.
to_list [Rel.Seq]
to_list ~limit s is, at most, the first limit elements of s.

unit [Rel.Dom]
unit is a domain for the () value.
unit [Rel]
unit is const Dom.unit ().

v [Rel_list.Make]
v l is l as a relational list.
v [Rel.Dom]
v ~name ~pp ~equal is a new domain named name using equal to test values for equality and pp to print them.
v1 [Rel.Query]
v1 [Rel.Fresh]
v2 [Rel.Query]
v2 [Rel.Fresh]
v3 [Rel.Query]
v3 [Rel.Fresh]
v4 [Rel.Query]
v4 [Rel.Fresh]
v5 [Rel.Query]
v5 [Rel.Fresh]
v6 [Rel.Query]
v6 [Rel.Fresh]

with_dom [Rel.Dom]
with_dom ~name ~pp d is domain d with name name and pretty-printer pp.