Ssreflect Users Discussion List

[Daniel Selsam <>]

Hi,

I thank you both very much for your help, and am still processing the 
responses. There are quite a lot of subtleties here, and it may take me a 
while to gain intuition for which challenges are due to design decisions in 
ssreflect that strongly favor ease of theory building, and which ones are 
inherent difficulties in unifying theorem proving and computer algebra. 

Thanks again,

Daniel 

----- Original Message -----
From: "Emilio Jesús Gallego Arias" <>
To: "Georges Gonthier" <>
Cc: "Daniel Selsam" <>, 
Sent: Tuesday, March 10, 2015 9:02:31 AM
Subject: Re: [ssreflect] Computing with bigops

Hi,

Thank you very much for the very nice code Georges, it is of great
help for people like myself, trying to learn how to use the libraries.

Best regards,
Emilio