dedukti

The Dedukti logical framework
IN THIS PACKAGE
Module Dtree
type case =
| CConst of int * Basic.name
| CDB of int * int
| CLam
type arg_pos = {
position : int;
depth : int;
}
type abstract_problem = arg_pos * int Basic.LList.t
type matching_problem =
| Syntactic of arg_pos Basic.LList.t
| MillerPattern of abstract_problem Basic.LList.t
val pp_matching_problem : matching_problem Basic.printer
type dtree =
| Switch of int * (case * dtree) list * dtree option
| 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 =
| HeadSymbolMismatch of Basic.loc * Basic.name * Basic.name
| ArityMismatch of Basic.loc * Basic.name
| ArityInnerMismatch of Basic.loc * Basic.ident * Basic.ident
val of_rules : Rule.rule_infos list -> ( int * dtree, dtree_error ) Basic.error