The Coq mailing list

["Soegtrop, Michael" <michael.soegtrop AT intel.com>]

Dear all,

 

I need to think a bit, but I guess the idea from Laurent will fix my case.

 

Regarding the various really short solutions: true for the simple example case these solutions are shorter, but for more real world cases the solution from Arnaud and Laurent is shorter, because you don't need to write down the expanded result (which is a few pages in my real case).

 

I also experimented with cbv delta. followed by several cbv iota; cbv beta. which also does the expansion step by step, but the idea from Laurent will bring me more directly to my goal and gives quite some flexibility.

 

Thanks & Best regards,

 

Michael