| Age | Commit message (Collapse) | Author |
|---|
|
Signed primitive integers defined on top of the existing unsigned ones
with two's complement.
The module Sint63 includes the theory of signed primitive integers that
differs from the unsigned case.
Additions to the kernel:
les (signed <=), lts (signed <), compares (signed compare),
divs (signed division), rems (signed remainder),
asr (arithmetic shift right)
(The s suffix is not used when importing the Sint63 module.)
The printing and parsing of primitive ints was updated and the
int63_syntax_plugin was removed (we use Number Notation instead).
A primitive int is parsed / printed as unsigned or signed depending on
the scope. In the default (Set Printing All) case, it is printed in
hexadecimal.
|
|
The smallcaps rendering was inexistent in the PDF version and did not
look good in the HTML version.
|
|
|
|
Update doc/sphinx/language/core/primitive.rst
Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com>
Add persistent data structure
Update doc/sphinx/language/core/primitive.rst
Co-authored-by: Hugo Herbelin <herbelin@users.noreply.github.com>
Update doc/sphinx/language/core/primitive.rst
Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com>
Update doc/sphinx/language/core/primitive.rst
Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com>
|
|
Persistent arrays expose a functional interface but are implemented
using an imperative data structure. The OCaml implementation is based on
Jean-Christophe Filliâtre's.
Co-authored-by: Benjamin Grégoire <Benjamin.Gregoire@inria.fr>
Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
|
|
|
