package msat
Library containing a SAT solver that can be parametrized by a theory
Install
Dune Dependency
Authors
Maintainers
Sources
v0.8.3.tar.gz
md5=d13411fc725e3b53343f7c389560fbdf
sha512=8ecc179e61a695c69bba5014f10e8c80b4366bec365ffe7e3274ab3d7510388f91c792ce5e7950f50f44fb556a4b66aa3cc19a745a57eac1dd09c12a0081916b
doc/msat.backend/Msat_backend/Coq/Make/argument-2-A/index.html
Parameter Make.A
Term printing for Coq
val prove_hyp : Format.formatter -> string -> S.clause -> unitval prove_lemma : Format.formatter -> string -> S.clause -> unitval prove_assumption : Format.formatter -> string -> S.clause -> unitProving function for hypotheses, lemmas and assumptions. prove_x fmt name x should prove x, and be such that after executing it, x is among the coq hypotheses under the name name. The hypothesis should be the encoding of the given clause, i.e for a clause a \/ not b \/ c, the proved hypothesis should be: ~ a -> ~ ~ b -> ~ c -> False , keeping the same order as the one in the atoms array of the clause.