Module Logtk.Dtree (.ml)

module Dtree: LogtkDtree


This module provides a simplification index, based on a perfect discrimination tree (see "the handbook of automated reasoning", chapter "term indexing", for instance).
module Make (E : LogtkIndex.EQUATION) : LogtkIndex.UNIT_IDX  with module E = E
module Default: LogtkIndex.UNIT_IDX  with module E = LogtkIndex.BasicEquation