From 24ccc118ccfb4c1223cd37bd43c9d26a77851176 Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Wed, 15 Mar 2017 03:11:23 +0100 Subject: 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. --- doc/stdlib/index-list.html.template | 1 + 1 file changed, 1 insertion(+) (limited to 'doc/stdlib') diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template index f448248468..0fa42cadad 100644 --- a/doc/stdlib/index-list.html.template +++ b/doc/stdlib/index-list.html.template @@ -226,6 +226,7 @@ through the Require Import command.

theories/Numbers/BinNums.v theories/Numbers/NumPrelude.v theories/Numbers/NaryFunctions.v + theories/Numbers/AltBinNotations.v theories/Numbers/DecimalFacts.v theories/Numbers/DecimalNat.v theories/Numbers/DecimalPos.v -- cgit v1.2.3