From 7497d4129775d15cdce862a0ac681c6400aabe54 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 6 Oct 2016 07:02:24 +0200 Subject: Logic library: Adding a characterization of excluded-middle in term of choice of a representative in a partition of bool. MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Also move a result about propositional extensionality from ClassicalFacts.v to PropExtensionalityFacts.v, generalizing it by symmetry. Also spotting typos (thanks to Théo). --- 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 9216c81fc..4a685a3b8 100644 --- a/doc/stdlib/index-list.html.template +++ b/doc/stdlib/index-list.html.template @@ -55,6 +55,7 @@ through the Require Import command.

theories/Logic/Description.v theories/Logic/Epsilon.v theories/Logic/IndefiniteDescription.v + theories/Logic/PropExtensionalityFacts.v theories/Logic/FunctionalExtensionality.v theories/Logic/ExtensionalityFacts.v theories/Logic/WeakFan.v -- cgit v1.2.3