package dedukti

  1. Overview
  2. Docs
On This Page
  1. Matching solver

Matching on terms

val d_matching : Basic.Debug.flag

Matching solver

exception NotUnifiable
val solve_miller : Dtree.miller_var -> Term.term -> Term.term

solve_miller var t Solves the matching problem X x1 ... xn = t where var represents the applied Miller variable X x1 ... xn. Raises NotUnifiable in case there is no solution.

module type Reducer = sig ... end
module type Matcher = sig ... end
module Make (R : Reducer) : Matcher

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