Equality configuration.

get_eq_config ss pos returns the current configuration for equality, used by tactics such as “rewrite” or “reflexivity”.

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 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.

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.

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.

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.

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.

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.

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).

replace_wild_by_tref t substitutes every wildcard of t by a fresh TRef.

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.