val signature_of_goal:
dbd:Mysql.dbd -> ProofEngineTypes.status -> UriManager.uri list
+val equations_for_goal:
+ dbd:Mysql.dbd -> ProofEngineTypes.status -> UriManager.uri list
+
val locate:
dbd:Mysql.dbd ->
?vars:bool -> string -> UriManager.uri list
-val hint:
- dbd:Mysql.dbd ->
- ?facts:bool ->
- ?signature:MetadataConstraints.term_signature ->
- ProofEngineTypes.status ->
- (UriManager.uri *
- (ProofEngineTypes.proof * ProofEngineTypes.goal list)) list
-
val experimental_hint:
dbd:Mysql.dbd ->
?facts:bool ->
val fwd_simpl: dbd:Mysql.dbd -> Cic.term -> UriManager.uri list
+val decomposables: dbd:Mysql.dbd -> (UriManager.uri * int) list