Ssreflect Users Discussion List

[Georges Gonthier <>]

  It does; the internal implementation recognizes a term of type True * (x = 
y) as a right-to-left rewrite rule (rewriting y to x); more generally, you 
can replace x = y by any rewritable type (e.g., a quantified tuple of Setoid 
relations).
  Given the current binding of the single constructor for True in Logic.v, 
this means you have to write
  rewrite (thm1, (I, thm2))
or possible
  rewrite (thm1, (Logic.I, thm2))
if I is bound locally (e.g., by a Variable I : finType Section-level 
declaraction).
  I've never been totally satisfied with this state of affairs, so I've not 
advertised the feature, and I've managed to avoid using it altogether in the 
library. Perhaps we could add definitions for True * E and (I, e) in 
ssreflect.v, and provide some kind of infix notation for the latter. I must 
confess I didn't do it because I couldn't come up with a good symbol for it: 
it would have to be short, intuitive and yet not conflict with any other user 
notation (this rules out -thm2) because there is no special notation "scope" 
that applies at the point the notation is used (it must be somehow possible 
to push an interpretation scope for the arguments of rewrite, but I wasn't 
able to figure out the API). Any suggestions?

  Georges

-----Original Message-----
From: Laurent Théry [] 
Sent: 27 May 2010 14:45
To: 
Subject: Re: dependent type error in rewrite


Hi,

There used to be (a long time ago :-), a way to add reversed theorem in 
multirewrite.
Something like:

rewrite (thm1, -thm2).

does this still exist?

--
Laurent