val make_active: Equality.equality list -> active_table
val make_passive: Equality.equality list -> passive_table
val add_to_passive: Equality.equality list -> passive_table -> passive_table
+val add_to_active:
+ Equality.equality_bag ->
+ active_table -> passive_table ->
+ Utils.environment -> Cic.term (* ty *) -> Cic.term -> Cic.metasenv ->
+ active_table * passive_table * Equality.equality_bag
val list_of_passive: passive_table -> Equality.equality list
+val list_of_active: active_table -> Equality.equality list
val simplify_equalities :
Equality.equality_bag ->
UriManager.uri ->
Utils.environment ->
Equality.equality list ->
- Equality.equality list
+ Equality.equality_bag * Equality.equality list
val pump_actives :
Cic.context ->
Equality.equality_bag ->
- int ->
active_table ->
passive_table ->
int ->
float ->
- active_table * passive_table * int
+ active_table * passive_table * Equality.equality_bag
val all_subsumed :
Equality.equality_bag ->
- int ->
ProofEngineTypes.status ->
active_table ->
passive_table ->
(Cic.substitution *
ProofEngineTypes.proof *
- ProofEngineTypes.goal list) list * int
+ ProofEngineTypes.goal list) list
val given_clause:
Equality.equality_bag ->
- int -> (* maxmeta *)
ProofEngineTypes.status ->
active_table ->
passive_table ->
(Cic.substitution *
ProofEngineTypes.proof *
ProofEngineTypes.goal list) option *
- active_table * passive_table * int
+ active_table * passive_table * Equality.equality_bag
+val solve_narrowing:
+ Equality.equality_bag ->
+ ProofEngineTypes.status ->
+ active_table ->
+ passive_table ->
+ int ->
+ (Cic.substitution *
+ ProofEngineTypes.proof *
+ ProofEngineTypes.goal list) option *
+ active_table * passive_table * Equality.equality_bag