package dedukti
Legend:
Library
Module
Module type
Parameter
Class
Class type
Library
Module
Module type
Parameter
Class
Class type
type abstract_problem = arg_pos * int Basic.LList.ttype matching_problem = | Syntactic of arg_pos Basic.LList.t| MillerPattern of abstract_problem Basic.LList.t
val pp_matching_problem : matching_problem Basic.printertype 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.printertype rw = Basic.name * int * dtreeval pp_rw : rw Basic.printertype 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