package libzipperposition

  1. Overview
  2. Docs
package libzipperposition
Legend:
Library
Module
Module type
Parameter
Class
Class type

The state of a proof, contains a set of active clauses (processed), a set of passive clauses (to be processed), and an ordering that is used for redundancy elimination.

module type S = ProofState_intf.S

Create a Proof State

module Make (C : Clause.S) : S with module C = C and module Ctx = C.Ctx