blob: d6fa75689b43ac32ac24d3b5953a642ad0ac1269 (
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
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
|
val euf_checker_modules : string list list
val certif_ops :
Term.constr array option ->
Term.constr lazy_t * Term.constr lazy_t * Term.constr lazy_t *
Term.constr lazy_t * Term.constr lazy_t * Term.constr lazy_t *
Term.constr lazy_t * Term.constr lazy_t * Term.constr lazy_t *
Term.constr lazy_t * Term.constr lazy_t * Term.constr lazy_t *
Term.constr lazy_t * Term.constr lazy_t * Term.constr lazy_t *
Term.constr lazy_t * Term.constr lazy_t * Term.constr lazy_t *
Term.constr lazy_t
val cCertif : Term.constr lazy_t
val ccertif : Term.constr lazy_t
val cchecker : Term.constr lazy_t
val cchecker_correct : Term.constr lazy_t
val cchecker_b_correct : Term.constr lazy_t
val cchecker_b : Term.constr lazy_t
val cchecker_eq_correct : Term.constr lazy_t
val cchecker_eq : Term.constr lazy_t
val compute_roots :
SmtAtom.Form.t list -> SmtAtom.Form.t SmtCertif.clause -> int list
val interp_uf :
(int, Term.constr) Hashtbl.t ->
(int, Term.constr) Hashtbl.t -> SmtAtom.Form.t list -> Term.constr
val interp_conseq_uf :
SmtAtom.Form.t list list * SmtAtom.Form.t list -> Term.types
val print_assm : Term.constr -> unit
val parse_certif :
Names.identifier ->
Names.identifier ->
Names.identifier ->
Names.identifier ->
Names.identifier ->
Names.identifier ->
Names.identifier ->
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 -> unit
val interp_roots : SmtAtom.Form.t list -> Term.constr
val theorem :
Names.identifier ->
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 -> unit
val checker :
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 -> unit
val build_body :
SmtAtom.Btype.reify_tbl ->
SmtAtom.Op.reify_tbl ->
SmtAtom.Atom.reify_tbl ->
SmtAtom.Form.reify ->
Term.constr ->
Term.constr ->
int * SmtAtom.Form.t SmtCertif.clause ->
Term.constr * Term.constr * (Names.identifier * Term.types) list
val build_body_eq :
SmtAtom.Btype.reify_tbl ->
SmtAtom.Op.reify_tbl ->
SmtAtom.Atom.reify_tbl ->
SmtAtom.Form.reify ->
Term.constr ->
Term.constr ->
Term.constr ->
int * SmtAtom.Form.t SmtCertif.clause ->
Term.constr * Term.constr * (Names.identifier * Term.types) list
val get_arguments : Term.constr -> Term.constr * Term.constr
val make_proof :
('a ->
'b ->
SmtAtom.Form.t -> SmtAtom.Form.t SmtCertif.clause * SmtAtom.Form.t -> 'c) ->
'a -> 'b -> SmtAtom.Form.reify -> SmtAtom.Form.t -> 'c
val core_tactic :
(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) ->
SmtAtom.Btype.reify_tbl ->
SmtAtom.Op.reify_tbl ->
SmtAtom.Atom.reify_tbl ->
SmtAtom.Form.reify ->
Environ.env -> Evd.evar_map -> Term.constr -> Structures.tactic
val tactic :
(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) ->
SmtAtom.Btype.reify_tbl ->
SmtAtom.Op.reify_tbl ->
SmtAtom.Atom.reify_tbl -> SmtAtom.Form.reify -> Structures.tactic
|
