- (NCic.term * NCic.term * NCic.metasenv * NCic.substitution) list
-
-type state
-val empty_state: state
-val forward_infer_step: state -> NCic.term -> NCic.term -> state
-val index_obj: state -> NUri.uri -> state
-val is_equation: NCic.metasenv ->
- NCic.substitution -> NCic.context -> NCic.term -> bool
-val paramod :
- #NRstatus.status ->
- NCic.metasenv -> NCic.substitution -> NCic.context ->
- state ->
- (NCic.term * NCic.term) ->
- (NCic.term * NCic.term * NCic.metasenv * NCic.substitution) list
-val fast_eq_check :
- #NRstatus.status ->
- NCic.metasenv -> NCic.substitution -> NCic.context ->
- state ->
- (NCic.term * NCic.term) ->
- (NCic.term * NCic.term * NCic.metasenv * NCic.substitution) list
-val demod :
- #NRstatus.status ->
- NCic.metasenv -> NCic.substitution -> NCic.context ->
- state ->
- (NCic.term * NCic.term) ->
- (NCic.term * NCic.term * NCic.metasenv * NCic.substitution) list