package dedukti

  1. Overview
  2. Docs

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


module R : Reducer


val solve_problem : Rule.rule_name -> Signature.t -> (int -> Term.term Stdlib.Lazy.t) -> (int -> Term.term Stdlib.Lazy.t list) -> Dtree.pre_matching_problem -> Term.term Stdlib.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.