package msat

You can search for identifiers within the package.

in-package search v0.2.0

Module `Msat_backend.Coq`Source

Coq Backend

This module provides an easy way to produce coq scripts corresponding to the resolution proofs output by the sat solver.

Sourcemodule type S = Backend_intf.S

Interface for exporting proofs.

Sourcemodule type Arg = sig ... end

Term printing for Coq

Source

module Make
  (S : Msat.S)
  (A : 
    Arg
      with type hyp := S.clause
       and type lemma := S.clause
       and type assumption := S.clause) : 
  S with type t := S.proof

Base functor to output Coq proofs

Source

module Simple
  (S : Msat.S)
  (A : 
    Arg
      with type hyp = S.formula list
       and type lemma := S.lemma
       and type assumption := S.formula) : 
  S with type t := S.proof

Simple functor to output Coq proofs

package msat

Module Msat_backend.CoqSource

Module `Msat_backend.Coq`Source