Re: [isabelle] Want to use Rep_Integ or lifting after [quot_del] in Int.thy



Coq and Isabelle/HOL are proof assistants, not programming languages. I can't imagine what gave you that idea. In Coq and Isabelle/HOL you write specifications, not code.

Larry Paulson


On 22 May 2013, at 14:16, Gottfried Barrow <gottfried.barrow at gmx.com> wrote:

> Thanks for your comment. I was comparing the formal, textbook construction of the integers, as in what you're listing, to concrete implementations of integers in programming languages, such as Coq, Isabelle/HOL, Haskell, or any other language, old or new, but especially new.





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.