We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent 0fe2a62 commit 6359797Copy full SHA for 6359797
1 file changed
src/plugin/features.mli
@@ -10,8 +10,8 @@ val get_goal_features : hhdef list (* hyps *) -> hhdef (* goal *) -> string list
10
val extract : hhdef list (* hyps *) -> hhdef list (* defs *) -> hhdef (* goal *) ->
11
string (* (temporary) file name *)
12
13
-val extract_given_lemmas : hhdef list (* hyps *) -> hhdef list (* defs *) -> hhdef list (* argus *) -> hhdef (* goal *) -> string (* *) ->
14
- hhdef list (* (temporary) file name *)
+val extract_given_lemmas : hhdef list (* hyps *) -> hhdef list (* defs *) -> hhdef list (* lemmas *) -> hhdef (* goal *) -> string (* ATP name *) ->
+ hhdef list (* used objects *)
15
16
val run_predict : string (* file name (from `extract`) *) -> hhdef list (* defs *) ->
17
int (* pred_num *) -> string (* pred_method *) ->
0 commit comments