package msat
Library containing a SAT solver that can be parametrized by a theory
Install
Dune Dependency
Authors
Maintainers
Sources
v0.8.1.tar.gz
md5=70159e4db67c5b3118fd765c478ffac8
sha512=dc92ad406270bac92caf9451bfeef6e396f0fed3af7cab102c6d2d2e09cc256cbbf728c2025e1cf6d9662a3eb0425aad75fe7f41d9413dccf1d520b38f964ef1
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.