val debug_matching : Debug.flagval intros : Term.term -> Term.term list * Term.vsymbol list * Term.termval term_decl : Theory.tdecl -> Term.termval with_terms :
trans_name:string ->
Ty.ty Ty.Mtv.t ->
Term.term Term.Mvs.t ->
Term.Mvs.key list ->
Term.term list ->
Ty.ty Ty.Mtv.t * Term.term Term.Mvs.tval matching_with_terms :
trans_name:string ->
Term.Svs.t ->
Term.Mvs.key list ->
Term.term ->
Term.term ->
Term.term list option ->
Ty.ty Ty.Mtv.t * Term.term Term.Mvs.tval apply : Decl.prsymbol -> Term.term list option -> Task.task Trans.tlistval rewrite_in :
bool ->
Term.term list ->
Decl.prsymbol ->
Decl.prsymbol ->
Task.task list Trans.transval find_target_prop : Decl.prsymbol option -> Decl.prsymbol Trans.transval rewrite :
Term.term list option ->
bool ->
Decl.prsymbol ->
Decl.prsymbol option ->
Task.task list Trans.transval rewrite_list :
Term.term list option ->
bool ->
bool ->
Decl.prsymbol list ->
Decl.prsymbol option ->
Task.task list Trans.transval detect_prop :
Decl.prsymbol ->
Decl.prop_kind ->
Decl.prsymbol option ->
boolval detect_prop_list :
Decl.prsymbol ->
Decl.prop_kind ->
Decl.prsymbol list option ->
boolval replace :
Term.term ->
Term.term ->
Decl.prsymbol list option ->
Task.task Trans.tlistval t_replace_app :
Term.lsymbol ->
(Term.Mvs.key list * Term.term) ->
Term.term ->
Term.termval t_ls_replace :
Term.lsymbol ->
(Term.Mvs.key list * Term.term) ->
Term.term ->
Term.termval unfold : Term.lsymbol -> Decl.prsymbol list option -> Task.task Trans.trans