coq-club AT inria.fr

Subject: The Coq mailing list

List archive

RE: [Coq-Club] avoid recursive expansion with simpl or cbv

From: "Soegtrop, Michael" <michael.soegtrop AT intel.com>
Cc: Coq Club <coq-club AT inria.fr>
Subject: RE: [Coq-Club] avoid recursive expansion with simpl or cbv
Date: Mon, 21 Oct 2013 14:04:11 +0000
Accept-language: de-DE, en-US

Dear Coq Users,

I used the method from Laurent as refined by Arnaud in my proof and it works like a charm. Just one remember and rewrite around the simpl is sufficient to control at which level the expansion shall stop. Very elegant!

Thanks Laurent and Arnaud for your help!

Best regards,

Michael

[Coq-Club] avoid recursive expansion with simpl or cbv, michael.soegtrop, 10/21/2013
- Re: [Coq-Club] avoid recursive expansion with simpl or cbv, Laurent Théry, 10/21/2013
  - Re: [Coq-Club] avoid recursive expansion with simpl or cbv, Arnaud Spiwack, 10/21/2013
    - Re: [Coq-Club] avoid recursive expansion with simpl or cbv, Nuno Gaspar, 10/21/2013
      - Re: [Coq-Club] avoid recursive expansion with simpl or cbv, Laurent Théry, 10/21/2013
      - Re: [Coq-Club] avoid recursive expansion with simpl or cbv, Robbert Krebbers, 10/21/2013
      - Re: [Coq-Club] avoid recursive expansion with simpl or cbv, Gert Smolka, 10/21/2013
        
        RE: [Coq-Club] avoid recursive expansion with simpl or cbv, Soegtrop, Michael, 10/21/2013
    - RE: [Coq-Club] avoid recursive expansion with simpl or cbv, Soegtrop, Michael, 10/21/2013