Legend:
Library
Module
Module type
Parameter
Class
Class type
Library
Module
Module type
Parameter
Class
Class type
package dedukti
Legend:
Library
Module
Module type
Parameter
Class
Class type
Library
Module
Module type
Parameter
Class
Class type
val solve_problem :
Rule.rule_name ->
Signature.t ->
(int -> Term.term Lazy.t) ->
(int -> Term.term Lazy.t list) ->
Dtree.pre_matching_problem ->
Term.term Lazy.t Basic.LList.t optionsolve_problem sg eq_conv ac_conv pb solves the pb matching problem using the given functions to convert positions in the stack to actual (lazy) terms.