The Coq mailing list

[Michael Day <mikeday AT yeslogic.com>]

Hi Hugo,

> Yes, most functions of Coq (the type-checker, the printer, and most
> auxiliary functions) are simply recursive. Rewriting all of them
> tail-recursively would increase the complexity of the code for a
> limited benefice since after all most use of large numbers is for
> computation and binary numbers are for this purpose much more
> efficient.

That makes a lot of sense. One issue I've found is that most examples 
use nat, for example the Coq'Art book uses nat exclusively. Moving to N 
can be a bit jarring for a beginner as the transition is not seamless; 
the < operator must be replaced with Ncompare or ?= for example.

Another question: is there any way to use hexadecimal integer literals? 
Perhaps some kind of notation trick?

Best regards,

Michael

--
Print XML with Prince!
http://www.princexml.com