Functor Rel_list.Make

module Make: 
functor (E : EL) -> sig .. end
Make (E) is a module for relational lists with elements of type E.
E : EL

Relational lists

type t = E.t list Rel.term 
The type for relational lists.
type e = E.t Rel.term 
The type for relational list elements.
val dom : E.t list Rel.dom

Term constructors

val empty : t
empty is the empty list.
val cons : e -> t -> t
cons x xs is the list x :: xs.
val v : E.t list -> t
v l is l as a relational list.

Relational operations

val is_empty : t -> Rel.goal
is_empty l is Rel.(empty = l).
val hd : t -> e -> Rel.goal
hd l x succeeds if x is the head of l.
val tl : t -> t -> Rel.goal
tl l xs succeeds if xs is the tail of l.
val append : t -> t -> t -> Rel.goal
append l0 l1 l succeeds if l1 appended to l0 is l.
val rev : t -> t -> Rel.goal
rev l r succeeds if r is the reverse list of l.