Up – Package index » dedukti » Library dedukti.kernel » Kernel » Matching » Make

Module `Matching.Make`Source

This is the default implementation. * It relies on the provided : * - whnf reduction strategy to flatten AC terms without digging to deep inside * - snf reduction strategy to perform higher order matching when necessary * - are_convertible convertibility test

Parameters

module R : Reducer

Signature

Source

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.