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') 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
  NatInt: -- cgit v1.2.3