Legend:
Library
Module
Module type
Parameter
Class
Class type
Library
Module
Module type
Parameter
Class
Class type
Implementation of the rewrite tactic.
val log_rewr : 'a Lplib.Base.outfmt -> 'a
type eq_config = {
symb_P : Core.Term.sym;
Encoding of propositions.
*)symb_T : Core.Term.sym;
Encoding of types.
*)symb_eq : Core.Term.sym;
Equality proposition.
*)symb_eqind : Core.Term.sym;
Induction principle on equality.
*)symb_refl : Core.Term.sym;
Reflexivity of equality.
*)}
Equality configuration.
val get_eq_config : Core.Sig_state.t -> Common.Pos.popt -> eq_config
get_eq_config ss pos
returns the current configuration for equality, used by tactics such as “rewrite” or “reflexivity”.
val get_eq_data :
eq_config ->
Common.Pos.popt ->
Core.Term.term ->
(Core.Term.term * Core.Term.term * Core.Term.term) * Core.Term.tvar array
get_eq_data pos cfg a
returns ((a,l,r),[v1;..;vn])
if a ≡ Π v1:A1,
.., Π vn:An, P (eq a l r)
and fails otherwise.
type to_subst = Core.Term.tvar array * Core.Term.term
Type of a term with the free variables that need to be substituted. It is usually used to store the LHS of a proof of equality, together with the variables that were quantified over.
val matches : Core.Term.term -> Core.Term.term -> bool
matches p t
instantiates the TRef
's of p
so that p
gets equal to t
and returns true
if all TRef
's of p
could be instantiated, and false
otherwise.
val matching_subs : to_subst -> Core.Term.term -> Core.Term.term array option
matching_subs (xs,p) t
attempts to match the pattern p
containing the variables xs
) with the term t
. If successful, it returns Some ts
where ts
is an array of terms such that substituting xs
by the corresponding elements of ts
in p
yields t
.
val find_subst : to_subst -> Core.Term.term -> Core.Term.term array option
find_subst (xs,p) t
tries to find the first instance of a subterm of t
matching p
. If successful, the function returns the array of terms by which xs
must substituted.
val find_subterm_matching : Core.Term.term -> Core.Term.term -> bool
find_subterm_matching p t
tries to find a subterm of t
that matches p
by instantiating the TRef
's of p
. In case of success, the function returns true
.
val bind_pattern : Core.Term.term -> Core.Term.term -> Core.Term.tbinder
bind_pattern p t
replaces in the term t
every occurence of the pattern p
by a fresh variable, and returns the binder on this variable.
val swap :
eq_config ->
Core.Term.term ->
Core.Term.term ->
Core.Term.term ->
Core.Term.term ->
Core.Term.term
swap cfg a r l t
returns a term of type P (eq a l r)
from a term t
of type P (eq a r l)
.
val replace_wild_by_tref : Core.Term.term -> Core.Term.term
replace_wild_by_tref t
substitutes every wildcard of t
by a fresh TRef
.
val rewrite :
Core.Sig_state.t ->
Core.Term.problem ->
Common.Pos.popt ->
Proof.goal_typ ->
bool ->
(Core.Term.term, Core.Term.tbinder) Parsing.Syntax.rw_patt option ->
Core.Term.term ->
Core.Term.term
rewrite ss p pos gt l2r pat t
generates a term for the refine tactic representing the application of the rewrite tactic to the goal type gt
. Every occurrence of the first instance of the left-hand side is replaced by the right-hand side of the obtained proof (or the reverse if l2r is false). pat
is an optional SSReflect pattern. t
is the equational lemma that is appied. It handles the full set of SSReflect patterns.