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.
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