Lists and conjunctions and disjunctions

Documentation on exports

list_to_conj(List,Conj,End)

Conj is the conjunction made up of the elements of List plus a final element End.

list_to_conj(A,B)

Examples:

```?- list_to_conj(A, a).

A = [a] ? ;

no
?- list_to_conj(A, (a,V,b)).

A = [a,V,b] ? ;

no
?- list_to_conj([A], B).

B = A ? ;

no
?- list_to_conj([a,A,b], B).

B = (a,A,b) ? ;

no
?- list_to_conj([], B).

B = true ? ;

no
```

Usage 1:list_to_conj(A,B)

Conj is the conjunction made up of the elements of List. The empty list is ([]) is true).

• The following properties should hold at call time:
A is a list.
B is a free variable.
• The following properties should hold upon exit:
Conjuntions

Usage 2:list_to_conj(A,B)

• The following properties should hold at call time:
A is a free variable.
Conjuntions
• The following properties should hold upon exit:
A is a list.

conj_to_list(Conj,List)

List is the list made up of the elements of conjunction Conj (true is []).

list_to_disj(A,B)

Examples:

```?- list_to_disj([a], A).

A = a ? ;

no
?- list_to_disj([a,B,b], A).

A = (a;B;b) ? ;

no
?- list_to_disj(A, (a)).

A = [a] ? ;

no
?- list_to_disj(A, (a;B;b)).

A = [a,B,b] ? ;

no
?-
```

Usage 1:list_to_disj(A,B)

Disj is the disjunction made up of the elements of List. ([] is false).

• The following properties should hold at call time:
A is a list.
B is a free variable.
• The following properties should hold upon exit:
Disjunctions

Usage 2:list_to_disj(A,B)

• The following properties should hold at call time:
A is a free variable.
Disjunctions
• The following properties should hold upon exit:
A is a list.

disj_to_list(Disj,List)

List is the list made up of the elements of disjunction Disj (true is []).

Turns a conjunctive (normal form) formula into a list (of lists of ...). As a side-effect, inner conjunctions get flattened. No special care for true.

Inverse of conj_to_llist/2. No provisions for anything else than a non-empty list on input (i.e., they will go `as are' in the output.

Turns a disjunctive (normal form) formula into a list (of lists of ...). As a side-effect, inner disjunctions get flattened. No special care for true.

Inverse of disj_to_llist/2. No provisions for anything else than a non-empty list on input (i.e., they will go `as are' in the output.

PREDICATEbody2list/2
No further documentation available for this predicate.

Usage 1:asbody_to_conj(A,B)

Transforms assertion body A into a conjuntion (B). It runs in both ways

• The following properties should hold at call time:

B is a free variable.
• The following properties should hold upon exit:
The usual prolog way of writing conjuntions and disjuntions in a body using ',' and ';'

Usage 2:asbody_to_conj(A,B)

• The following properties should hold at call time:
A is a free variable.
The usual prolog way of writing conjuntions and disjuntions in a body using ',' and ';'
• The following properties should hold upon exit:

No further documentation available for this predicate.

Usage:

The usual prolog way of writing conjuntions and disjuntions in a body using ',' and ';'

REGTYPEt_conj/1

Usage:

Conjuntions

REGTYPEt_disj/1

Usage:

Disjunctions

No further documentation available for this predicate.

Documentation on imports

This module has the following direct dependencies: