Ssreflect Users Discussion List

[Enrico Tassi <>]

On Mon, Feb 22, 2016 at 02:45:32PM +0100, Assia Mahboubi wrote:
> Hello Georges (and list),
> 
> reading your message again:
> 
> Le 22/02/2016 12:20, Georges Gonthier a écrit :
> 
> >    The grouping of pairs does not affect the selection strategy, but it 
> > does make it easier include one rule set in another, revrse the direction 
> > of a rule subset, 
> 
> I did not understand what "reverse the direction of a rule subset" means? 
> Since
> multi-rules are nested pairs, how could we reverse one of the components?

It was added "late", probably after you wrote the section in the manual.

  Axiom x : nat.
  Axiom E1 : 1 = x.
  Axiom E2 : 2 = x.
  
  Goal x = 7.
  rewrite (=^~ (E1, E2)).

The =^~ operator flips the direction *of an entire set of rules*,
weather it is named or not.

No idea if this feature is used somewhere.

Ciao
-- 
Enrico Tassi