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
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
(** @canonical Logtk.AllocCache *)
module AllocCache = Logtk__AllocCache
(** @canonical Logtk.Binder *)
module Binder = Logtk__Binder
(** @canonical Logtk.Builtin *)
module Builtin = Logtk__Builtin
(** @canonical Logtk.Cnf *)
module Cnf = Logtk__Cnf
(** @canonical Logtk.Comparison *)
module Comparison = Logtk__Comparison
(** @canonical Logtk.Compute_prec *)
module Compute_prec = Logtk__Compute_prec
(** @canonical Logtk.Congruence *)
module Congruence = Logtk__Congruence
(** @canonical Logtk.Congruence_intf *)
module Congruence_intf = Logtk__Congruence_intf
(** @canonical Logtk.DBEnv *)
module DBEnv = Logtk__DBEnv
(** @canonical Logtk.Defined_pos *)
module Defined_pos = Logtk__Defined_pos
(** @canonical Logtk.Dtree *)
module Dtree = Logtk__Dtree
(** @canonical Logtk.FV_tree *)
module FV_tree = Logtk__FV_tree
(** @canonical Logtk.FeatureVector *)
module FeatureVector = Logtk__FeatureVector
(** @canonical Logtk.Fingerprint *)
module Fingerprint = Logtk__Fingerprint
(** @canonical Logtk.Flex_state *)
module Flex_state = Logtk__Flex_state
(** @canonical Logtk.HO_unif *)
module HO_unif = Logtk__HO_unif
(** @canonical Logtk.HVar *)
module HVar = Logtk__HVar
(** @canonical Logtk.Hash *)
module Hash = Logtk__Hash
(** @canonical Logtk.Hashcons *)
module Hashcons = Logtk__Hashcons
(** @canonical Logtk.Head *)
module Head = Logtk__Head
(** @canonical Logtk.IArray *)
module IArray = Logtk__IArray
(** @canonical Logtk.ID *)
module ID = Logtk__ID
(** @canonical Logtk.Ind_ty *)
module Ind_ty = Logtk__Ind_ty
(** @canonical Logtk.Index *)
module Index = Logtk__Index
(** @canonical Logtk.Index_intf *)
module Index_intf = Logtk__Index_intf
(** @canonical Logtk.InnerTerm *)
module InnerTerm = Logtk__InnerTerm
(** @canonical Logtk.Input_format *)
module Input_format = Logtk__Input_format
(** @canonical Logtk.Int_lit *)
module Int_lit = Logtk__Int_lit
(** @canonical Logtk.Interfaces *)
module Interfaces = Logtk__Interfaces
(** @canonical Logtk.Lambda *)
module Lambda = Logtk__Lambda
(** @canonical Logtk.LazyList *)
module LazyList = Logtk__LazyList
(** @canonical Logtk.Literal *)
module Literal = Logtk__Literal
(** @canonical Logtk.Literals *)
module Literals = Logtk__Literals
(** @canonical Logtk.Monome *)
module Monome = Logtk__Monome
(** @canonical Logtk.Multiset *)
module Multiset = Logtk__Multiset
(** @canonical Logtk.Multiset_intf *)
module Multiset_intf = Logtk__Multiset_intf
(** @canonical Logtk.Multisets *)
module Multisets = Logtk__Multisets
(** @canonical Logtk.NPDtree *)
module NPDtree = Logtk__NPDtree
(** @canonical Logtk.Options *)
module Options = Logtk__Options
(** @canonical Logtk.Ordering *)
module Ordering = Logtk__Ordering
(** @canonical Logtk.Ordinal *)
module Ordinal = Logtk__Ordinal
(** @canonical Logtk.Output_format *)
module Output_format = Logtk__Output_format
(** @canonical Logtk.ParseLocation *)
module ParseLocation = Logtk__ParseLocation
(** @canonical Logtk.Polynomial *)
module Polynomial = Logtk__Polynomial
(** @canonical Logtk.Position *)
module Position = Logtk__Position
(** @canonical Logtk.Precedence *)
module Precedence = Logtk__Precedence
(** @canonical Logtk.Proof *)
module Proof = Logtk__Proof
(** @canonical Logtk.Rat_lit *)
module Rat_lit = Logtk__Rat_lit
(** @canonical Logtk.Rewrite *)
module Rewrite = Logtk__Rewrite
(** @canonical Logtk.SLiteral *)
module SLiteral = Logtk__SLiteral
(** @canonical Logtk.STerm *)
module STerm = Logtk__STerm
(** @canonical Logtk.Scoped *)
module Scoped = Logtk__Scoped
(** @canonical Logtk.Signal *)
module Signal = Logtk__Signal
(** @canonical Logtk.Signature *)
module Signature = Logtk__Signature
(** @canonical Logtk.Skolem *)
module Skolem = Logtk__Skolem
(** @canonical Logtk.Statement *)
module Statement = Logtk__Statement
(** @canonical Logtk.Subst *)
module Subst = Logtk__Subst
(** @canonical Logtk.Term *)
module Term = Logtk__Term
(** @canonical Logtk.Test_prop *)
module Test_prop = Logtk__Test_prop
(** @canonical Logtk.Type *)
module Type = Logtk__Type
(** @canonical Logtk.TypeInference *)
module TypeInference = Logtk__TypeInference
(** @canonical Logtk.TypedSTerm *)
module TypedSTerm = Logtk__TypedSTerm
(** @canonical Logtk.Unif *)
module Unif = Logtk__Unif
(** @canonical Logtk.Unif_constr *)
module Unif_constr = Logtk__Unif_constr
(** @canonical Logtk.Unif_intf *)
module Unif_intf = Logtk__Unif_intf
(** @canonical Logtk.Unif_subst *)
module Unif_subst = Logtk__Unif_subst
(** @canonical Logtk.UnionFind *)
module UnionFind = Logtk__UnionFind
(** @canonical Logtk.UntypedAST *)
module UntypedAST = Logtk__UntypedAST
(** @canonical Logtk.Util *)
module Util = Logtk__Util
(** @canonical Logtk.Var *)
module Var = Logtk__Var