ssreflect - Re: [ssreflect] [rewrite foo in hyp] weirdness

Subject: Ssreflect Users Discussion List

List archive

Re: [ssreflect] [rewrite foo in hyp] weirdness

From: Enrico Tassi <>
To:
Subject: Re: [ssreflect] [rewrite foo in hyp] weirdness
Date: Thu, 14 Jan 2016 16:11:55 +0100
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None ; spf=None ; spf=None
Ironport-phdr: 9a23:dd9SOBIbJcDQ7/CCadmcpTZWNBhigK39O0sv0rFitYgULvTxwZ3uMQTl6Ol3ixeRBMOAu6wC27ud7fCocFdDyKjCmUhKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TWM5DIfUi/yKRBybrysXNWC0YLnhqvsq9X6WEZhunmUWftKNhK4rAHc5IE9oLBJDeIP8CbPuWZCYO9MxGlldhq5lhf44dqsrtY4q3wD86Fpy8kVSr7gcqo8QLdEJDE9KSU04tfqvF/CSxGO7z0SSDY4iB1NViXD9hDxWd/NuzDht6Ip1S+APMbxC6w9Qi+jx6ZtUh7hzikdYW1quFrLg9B92foI6CmqoAZyltbZ

On Thu, Jan 14, 2016 at 04:03:07PM +0100, Robbert Krebbers wrote:
> >then we pass the ball to Coq's rewrite anyway and let it complain"
> Will we then still benefit from ssr's subexpression matching when rewriting
> with setoid relations/partial orders?

Yes. Still there is a limitation: ssreflect's patterns do not operate
under binders.

Best,
--
Enrico Tassi

[ssreflect] [rewrite foo in hyp] weirdness, Robbert Krebbers, 01/13/2016
- Re: [ssreflect] [rewrite foo in hyp] weirdness, Emilio Jesús Gallego Arias, 01/13/2016
  - Re: [ssreflect] [rewrite foo in hyp] weirdness, Robbert Krebbers, 01/13/2016
    - RE: [ssreflect] [rewrite foo in hyp] weirdness, Georges Gonthier, 01/13/2016
      - Re: [ssreflect] [rewrite foo in hyp] weirdness, Robbert Krebbers, 01/13/2016
      - Re: [ssreflect] [rewrite foo in hyp] weirdness, Enrico Tassi, 01/14/2016
        
        Re: [ssreflect] [rewrite foo in hyp] weirdness, Robbert Krebbers, 01/14/2016
        
        Re: [ssreflect] [rewrite foo in hyp] weirdness, Enrico Tassi, 01/14/2016
        
        Re: [ssreflect] [rewrite foo in hyp] weirdness, Robbert Krebbers, 01/14/2016
        
        RE: [ssreflect] [rewrite foo in hyp] weirdness, Georges Gonthier, 01/14/2016

List archive

Re: [ssreflect] [rewrite foo in hyp] weirdness