Helper function which just tries to rewrite e using the equality r without assigning any
metavariables in the tactic state, and without creating any metavariables which cannot be
discharged by cfg.discharger in the process.
Returns true if the argument is a proof that the entire expression was rewritten.
This is a bit of a hack: we manually inspect the proof that rewrite_core produced, and deduce from
that whether or not the entire expression was rewritten.
Function which tries to perform the rewrite associated to the equality r : expr × bool (the
bool indicates whether we should flip the equality first), at the position pointed to by
l : expr_lens, by rewriting e : expr. If this succeeds, rewrite_at_lens computes (by unwinding
l) a proof that the entire expression represented by l.fill e is equal to the entire expression
l.fill f, where f is the expr which has replaced e due to the rewrite. It then returns the
singleton list containing this rewrite (and the tracking data needed to reconstruct it directly). If
it fails, it just returns the empty list.
List of all rewrites of an expression e by r : expr × bool.
Here r.1 is the substituting expression and r.2 flags the direction of the rewrite.
Lazy list of all rewrites of an expression e by r : expr × bool.
Here r.1 is the substituting expression and r.2 flags the direction of the rewrite.