diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-04-04 17:10:45 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-04-04 17:10:45 +0000 |
| commit | 5fb2d53414158b2d6ca97f3d33bf38fbd938252d (patch) | |
| tree | dac37f720dc575c1139cbba6371d6abb0236f5fa /theories/Logic/ChoiceFacts.v | |
| parent | bc8728f0762f7e39f779c677679a8bc351a4290a (diff) | |
Correction problème de compil (blast.ml)
Correction bugs commentaires pour coqdoc (ChoiceFacts.v)
Test-suite
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10756 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Logic/ChoiceFacts.v')
| -rw-r--r-- | theories/Logic/ChoiceFacts.v | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/theories/Logic/ChoiceFacts.v b/theories/Logic/ChoiceFacts.v index 20ffe7b5a..3f4c4354b 100644 --- a/theories/Logic/ChoiceFacts.v +++ b/theories/Logic/ChoiceFacts.v @@ -29,7 +29,7 @@ description principles - OAC_rel = "omniscient" relational form of the (non extensional) axiom of choice - OAC_fun = "omniscient" functional form of the (non extensional) axiom of choice - (called AC* in Bell [Bell]) + (called AC* in Bell [[Bell]]) - OAC! - ID_iota = intuitionistic definite description @@ -43,7 +43,7 @@ description principles (an unconstrained generalisation of the constructive principle of independence of premises) - Drinker = drinker's paradox (small form) - (called Ex in Bell [Bell]) + (called Ex in Bell [[Bell]]) We let also @@ -75,10 +75,10 @@ Table of contents References: -[Bell] John L. Bell, Choice principles in intuitionistic set theory, +[[Bell]] John L. Bell, Choice principles in intuitionistic set theory, unpublished. -[Bell93] John L. Bell, Hilbert's Epsilon Operator in Intuitionistic +[[Bell93]] John L. Bell, Hilbert's Epsilon Operator in Intuitionistic Type Theories, Mathematical Logic Quarterly, volume 39, 1993. [Carlstrøm05] Jesper Carlstrøm, Interpreting descriptions in @@ -426,7 +426,7 @@ Qed. (** AC_fun + Drinker = OAC_fun *) -(** This was already observed by Bell [Bell] *) +(** This was already observed by Bell [[Bell]] *) Lemma omniscient_fun_choice_imp_small_drinker : OmniscientFunctionalChoice -> SmallDrinker'sParadox. @@ -754,17 +754,17 @@ be applied on the same Type universes on both sides of the first (**********************************************************************) (** * Excluded-middle + definite description => computational excluded-middle *) -(** The idea for the following proof comes from [ChicliPottierSimpson02] *) +(** The idea for the following proof comes from [[ChicliPottierSimpson02]] *) (** Classical logic and axiom of unique choice (i.e. functional - relation reification), as shown in [ChicliPottierSimpson02], + relation reification), as shown in [[ChicliPottierSimpson02]], implies the double-negation of excluded-middle in [Set] (which is incompatible with the impredicativity of [Set]). We adapt the proof to show that constructive definite description transports excluded-middle from [Prop] to [Set]. - [ChicliPottierSimpson02] Laurent Chicli, Loïc Pottier, Carlos + [[ChicliPottierSimpson02]] Laurent Chicli, Loïc Pottier, Carlos Simpson, Mathematical Quotients and Quotient Types in Coq, Proceedings of TYPES 2002, Lecture Notes in Computer Science 2646, Springer Verlag. *) |