Up – Package index » dedukti » Library dedukti.kernel » Kernel » Reduction » Make » M

Parameter `Make.M`

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 option

solve_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.