package dedukti

  1. Overview
  2. Docs
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.

OCaml

Innovation. Community. Security.