On This Page
Legend:
Library
Module
Module type
Parameter
Class
Class type
Library
Module
Module type
Parameter
Class
Class type
package dedukti
On This Page
Legend:
Library
Module
Module type
Parameter
Class
Class type
Library
Module
Module type
Parameter
Class
Class type
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
Signature
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.
On This Page