diff options
Diffstat (limited to 'tactics/setoid_replace.mli')
| -rw-r--r-- | tactics/setoid_replace.mli | 64 |
1 files changed, 57 insertions, 7 deletions
diff --git a/tactics/setoid_replace.mli b/tactics/setoid_replace.mli index 854fa478..5dc691a9 100644 --- a/tactics/setoid_replace.mli +++ b/tactics/setoid_replace.mli @@ -6,22 +6,72 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: setoid_replace.mli,v 1.3.6.2 2005/01/21 17:14:11 herbelin Exp $ i*) +(*i $Id: setoid_replace.mli 6621 2005-01-21 17:24:37Z herbelin $ i*) open Term open Proof_type open Topconstr +open Names + +type relation = + { rel_a: constr ; + rel_aeq: constr; + rel_refl: constr option; + rel_sym: constr option; + rel_trans : constr option; + rel_quantifiers_no: int (* it helps unification *); + rel_X_relation_class: constr; + rel_Xreflexive_relation_class: constr + } + +type 'a relation_class = + Relation of 'a (* the [rel_aeq] of the relation or the relation*) + | Leibniz of constr option (* the [carrier] (if [eq] is partially instantiated)*) + +type 'a morphism = + { args : (bool option * 'a relation_class) list; + output : 'a relation_class; + lem : constr; + morphism_theory : constr + } + +type morphism_signature = (bool option * constr_expr) list * constr_expr + +val pr_morphism_signature : morphism_signature -> Pp.std_ppcmds + +val register_replace : (constr -> constr -> tactic) -> unit +val register_general_rewrite : (bool -> constr -> tactic) -> unit + +val print_setoids : unit -> unit val equiv_list : unit -> constr list +val default_relation_for_carrier : + ?filter:(relation -> bool) -> types -> relation relation_class +(* [default_morphism] raises [Not_found] *) +val default_morphism : + ?filter:(constr morphism -> bool) -> constr -> relation morphism -val setoid_replace : constr -> constr -> constr option -> tactic +val setoid_replace : + constr option -> constr -> constr -> new_goals:constr list -> tactic +val setoid_replace_in : + identifier -> constr option -> constr -> constr -> new_goals:constr list -> + tactic -val setoid_rewriteLR : constr -> tactic +val general_s_rewrite : bool -> constr -> new_goals:constr list -> tactic +val general_s_rewrite_in : + identifier -> bool -> constr -> new_goals:constr list -> tactic -val setoid_rewriteRL : constr -> tactic +val setoid_reflexivity : tactic +val setoid_symmetry : tactic +val setoid_symmetry_in : identifier -> tactic +val setoid_transitivity : constr -> tactic -val general_s_rewrite : bool -> constr -> tactic +val add_relation : + Names.identifier -> constr_expr -> constr_expr -> constr_expr option -> + constr_expr option -> constr_expr option -> unit -val add_setoid : constr_expr -> constr_expr -> constr_expr -> unit +val add_setoid : + Names.identifier -> constr_expr -> constr_expr -> constr_expr -> unit -val new_named_morphism : Names.identifier -> constr_expr -> unit +val new_named_morphism : + Names.identifier -> constr_expr -> morphism_signature option -> unit |