blob: 95959dae98807e2fe4b1906cb91ab017a5b83000 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
|
val debug : bool
val import_trace :
SmtAtom.Atom.reify_tbl -> SmtAtom.Form.reify -> string ->
(SmtAtom.Form.t SmtCertif.clause * SmtAtom.Form.t) option ->
SmtAtom.Form.t list -> int * SmtAtom.Form.t SmtCertif.clause
val clear_all : unit -> unit
val import_all :
string ->
string ->
SmtBtype.reify_tbl * SmtAtom.Op.reify_tbl * SmtAtom.Atom.reify_tbl *
SmtAtom.Form.reify * SmtAtom.Form.t list * int *
SmtAtom.Form.t SmtCertif.clause
val parse_certif :
Names.identifier ->
Names.identifier ->
Names.identifier ->
Names.identifier ->
Names.identifier ->
Names.identifier -> Names.identifier -> string -> string -> unit
val theorem : Names.identifier -> string -> string -> unit
val checker : string -> string -> unit
val export :
out_channel ->
SmtBtype.reify_tbl -> SmtAtom.Op.reify_tbl ->
SmtAtom.Form.t list -> unit
val call_verit :
SmtBtype.reify_tbl ->
SmtAtom.Op.reify_tbl ->
SmtAtom.Atom.reify_tbl ->
SmtAtom.Form.reify ->
(SmtAtom.Form.t SmtCertif.clause * SmtAtom.Form.t) option ->
SmtAtom.Form.t list ->
int * SmtAtom.Form.t SmtCertif.clause
val tactic : Term.constr list -> Structures.constr_expr list -> Structures.tactic
|