blob: 2ec830c529521a0d79a42990743e1c996bc86b31 (
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
|
val debug : bool
val import_trace :
string ->
(SmtAtom.Form.t SmtCertif.clause * SmtAtom.Form.t) option ->
int * SmtAtom.Form.t SmtCertif.clause
val clear_all : unit -> unit
val import_all :
string ->
string ->
SmtAtom.Btype.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 ->
SmtAtom.Btype.reify_tbl -> SmtAtom.Op.reify_tbl -> SmtAtom.Form.t -> unit
val call_verit :
SmtAtom.Btype.reify_tbl ->
SmtAtom.Op.reify_tbl ->
SmtAtom.Form.t ->
SmtAtom.Form.t SmtCertif.clause * SmtAtom.Form.t ->
int * SmtAtom.Form.t SmtCertif.clause
val tactic : unit -> Proof_type.tactic
|
