diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-08-02 10:10:33 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-08-02 10:10:33 +0000 |
| commit | 42fdbab0d8c6266ba596f07d6fa482eb29736d44 (patch) | |
| tree | 548190ef9445adea5454fb324cb110b222aceec5 /printing | |
| parent | fc6c6a6f4c0e9365a3040c3fae380f94af184fd0 (diff) | |
Bigint: new functions of_int and to_int, 2nd arg of pow in int
* Many of_string and to_string could be replaced by of_int and to_int
when the number isn't too large. NB: to_int may raise a Failure
if the number is larger than max_int.
* In numbers_syntax, computing the height of bigN trees via bigint
is *really* overkill, int should be enough there : this limits
printable/parsable bigN to (2^31)^(2^max_int) ...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15669 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'printing')
0 files changed, 0 insertions, 0 deletions