package coq-core

  1. Overview
  2. Docs
The Coq Proof Assistant -- Core Binaries and Tools

Install 

dune-project
 Dependency

coq.inria.fr Readme Edit opam file Versions (11)

Authors

  1. T
    The Coq development team, INRIA, CNRS, and contributors

Maintainers

  1. T
    The Coq development team <coqdev@inria.fr>

Sources

coq-8.18.0.tar.gz
md5=8d852367b54f095d9fbabd000304d450
sha512=46922d5f2eb6802a148a52fd3e7f0be8370c93e7bc33cee05cf4a2044290845b10ccddbaa306f29c808e7c5019700763e37e45ff6deb507b874a4348010fed50

doc/coq-core.interp/NumTok/index.html

Module NumTokSource

Numbers in different forms: signed or unsigned, possibly with fractional part and exponent.

Numbers are represented using raw strings of (hexa)decimal literals and a separate sign flag.

Note that this representation is not unique, due to possible multiple leading or trailing zeros, and -0 = +0, for instances. The reason to keep the number exactly as it was parsed is that specific notations can be declared for specific numbers (e.g. Notation "0" := False, or Notation "00" := (nil,nil), or Notation "2e1" := ...). Those notations override the generic interpretation as number. So, one has to record the form of the number which exactly matches the notation.

Sourcetype sign =
  1. | SPlus
  2. | SMinus
Sourcetype num_class =
  1. | CDec
  2. | CHex
Sourcetype 'a exp =
  1. | EDec of 'a
  2. | EBin of 'a
String representation of a natural number
Sourcemodule UnsignedNat : sig ... end
String representation of a signed natural number
Sourcemodule SignedNat : sig ... end
Unsigned decimal numbers
Sourcemodule Unsigned : sig ... end
Signed decimal numbers
Sourcemodule Signed : sig ... end