Numeral Notation for nat

 This parsing/printing method for nat should be just as fast as
 the previous dedicated code. Moreover, we could now parse large
 literals as nat numbers, by leaving them in a half-abstract form
 such as (Nat.of_uint 123456). This form is convertible to the
 closed (S (S (S ...))) form, so it shouldn't be a big deal for
 compatibility, except for if some Ltac stuff relies on (S ...) to be
 present after parsing. Of course, forcing the computation of
 a (Nat.of_uint ....) may take a while or raise a Stack Overflow.

0 files changed, 0 insertions, 0 deletions