Structs

A literal origin can be uniquely identified through its source clause and its index in the clause body

A proof tree consist of

Result of building the SLD tree.

An SLD tree consists of

Enums

In this usage, a ‘clause’ represents some method of resolution.

Traits

Functions

Returns a tree that contains both successful and failed paths, also, any resolution errors. To save on memory usage, can avoid storing the failed paths by passing false to store_full_tree.