Ssreflect Users Discussion List

[Georges Gonthier <>]

Hello,

The documentation is a bit brief in this respect. The planned behaviour for
  rewrite {occs}[range]/term
is:
  - match all subterms that match "range"
  - use "occs" to select occurrences of "range"
  - within the selected occurrences of "range" only,
    match occurrences of "term"
  - in those occurrences of "term", unfold the head constant
  - beta-iota simplify (zeta-simplify as well if {occs} is omitted)
As usual, the value of any omitted term ("_") is fixed by the first match.
  When the [range] switch is omitted, "range" defaults to "term", and 
currently only this case is (correctly) implemented. It may, however, be 
sufficient for your purposes.

   Best,

Georges


-----Original Message-----
From:  []
Sent: 19 June 2008 10:04
To: 
Subject: redex switch + unfold <r-item>


Hello.

Will the combination of redex switch and unfold <r-item> be implemented soon?
(ref: Page 45 in the documentation)

The reply will determine whether I will aggressively use
logical equivalence <->, which is already comfortably handled
by ssreflect's rewrite tactics, or abbreviations;
but I prefer abbreviations to benefit from ssreflect's set tactics.

With best regards,
Keiko