From 53720903b96f9616f8bd53318575e8bcc13c6fce Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Sat, 4 Apr 2020 22:36:02 +0200 Subject: Decimal: specify numeral notation for Q --- 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 4a62888552..340e855a05 100644 --- a/doc/stdlib/index-list.html.template +++ b/doc/stdlib/index-list.html.template @@ -235,6 +235,7 @@ through the Require Import command.
theories/Numbers/DecimalPos.v theories/Numbers/DecimalN.v theories/Numbers/DecimalZ.v + theories/Numbers/DecimalQ.v theories/Numbers/DecimalString.v -- cgit v1.2.3 From 0ee6e30022e5b5b244f5d9cd16acb6017817a6c0 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Sat, 28 Mar 2020 14:25:27 +0100 Subject: [doc] Add hexadecimal numerals --- doc/stdlib/index-list.html.template | 2 ++ 1 file changed, 2 insertions(+) (limited to 'doc/stdlib') diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template index 340e855a05..8db6b63273 100644 --- a/doc/stdlib/index-list.html.template +++ b/doc/stdlib/index-list.html.template @@ -21,6 +21,8 @@ through the Require Import command. theories/Init/Byte.v theories/Init/Nat.v theories/Init/Decimal.v + theories/Init/Hexadecimal.v + theories/Init/Numeral.v theories/Init/Peano.v theories/Init/Specif.v theories/Init/Tactics.v -- cgit v1.2.3 From da4a78d9fe25b000005a968d17c2e17bb42b71f4 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Thu, 2 Apr 2020 15:42:32 +0200 Subject: Hexadecimal: proofs that conversions from/to nat,N,Z and Q are bijections --- doc/stdlib/index-list.html.template | 6 ++++++ 1 file changed, 6 insertions(+) (limited to 'doc/stdlib') diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template index 8db6b63273..7896b59a8b 100644 --- a/doc/stdlib/index-list.html.template +++ b/doc/stdlib/index-list.html.template @@ -239,6 +239,12 @@ through the Require Import command. theories/Numbers/DecimalZ.v theories/Numbers/DecimalQ.v theories/Numbers/DecimalString.v + theories/Numbers/HexadecimalFacts.v + theories/Numbers/HexadecimalNat.v + theories/Numbers/HexadecimalPos.v + theories/Numbers/HexadecimalN.v + theories/Numbers/HexadecimalZ.v + theories/Numbers/HexadecimalQ.v