Howdy, ri...@happyleptic.org skribis:
> but I > understand that you could be very interested in Coq proving that a > complex recursive algorithm eventually terminates, while you don't care > much about the type checking. Actually, I just meant to say that type-checking is one of the many checks one may want the compiler to perform automatically. Ludo’.
