Ssreflect Users Discussion List

[Georges Gonthier <>]

  The feature itself isn't a late addition, since it was supported from day 1 
by the multirule rewrite code, long before Enrico took over. What's more 
recent is the (=^~ rule) syntax for what used to be written more primitively 
as (I, rule), to account for the increasing use of 'I' as a section or proof 
variable (obquiz: guess how reversal is encoded).
     Cheers,
Georges

-----Original Message-----
From: 

 
[mailto:]
 On Behalf Of Assia Mahboubi
Sent: 22 February 2016 15:19
To: 

Subject: Re: [ssreflect] ssreflect and omega

Hi Enrico,

thanks for the fast answer.

Le 22/02/2016 15:12, Enrico Tassi a écrit :
> 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.

Hum... and it seems it is not in the changes log either... But it is indeed 
briefly mentioned in ssreflect.v.

https://github.com/math-comp/math-comp/blob/master/mathcomp/ssreflect/ssreflect.v#L21

[...]

> No idea if this feature is used somewhere.

It is, as early as in seq.v:

https://github.com/math-comp/math-comp/blob/master/mathcomp/ssreflect/seq.v#L1577

or path.v:

https://github.com/math-comp/math-comp/blob/master/mathcomp/ssreflect/path.v#L789

Ok, better late than never, I will update the manual accordingly as soon as 
possible.

Cheers,

assia