package coq-core

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

Install

Dune Dependency

Authors

Maintainers

Sources

coq-8.20.1.tar.gz
md5=0cfaa70f569be9494d24c829e6555d46
sha512=8ee967c636b67b22a4f34115871d8f9b9114df309afc9ddf5f61275251088c6e21f6cf745811df75554d30f4cebb6682f23eeb2e88b771330c4b60ce3f6bf5e2

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
OCaml

Innovation. Community. Security.