package dedukti

  1. Overview
  2. Docs
type case =
  1. | CConst of int * Basic.name
  2. | CDB of int * int
  3. | CLam
type arg_pos = {
  1. position : int;
  2. depth : int;
}
type abstract_problem = arg_pos * int Basic.LList.t
type matching_problem =
  1. | Syntactic of arg_pos Basic.LList.t
  2. | MillerPattern of abstract_problem Basic.LList.t
val pp_matching_problem : matching_problem Basic.printer
type dtree =
  1. | Switch of int * (case * dtree) list * dtree option
  2. | Test of Rule.rule_name * matching_problem * Rule.constr list * Term.term * dtree option
val pp_dtree : dtree Basic.printer
type rw = Basic.name * int * dtree
val pp_rw : rw Basic.printer
type dtree_error =
  1. | HeadSymbolMismatch of Basic.loc * Basic.name * Basic.name
  2. | ArityMismatch of Basic.loc * Basic.name
  3. | ArityInnerMismatch of Basic.loc * Basic.ident * Basic.ident
val of_rules : Rule.rule_infos list -> (int * dtree, dtree_error) Basic.error