Logic « theories - coq - the Coq proof assistant

Mode	Name	Size
-rw-r--r--	Berardi.v	4130	log plain
-rw-r--r--	ChoiceFacts.v	48313	log plain
-rw-r--r--	Classical.v	666	log plain
-rw-r--r--	ClassicalChoice.v	2057	log plain
-rw-r--r--	ClassicalDescription.v	3054	log plain
-rw-r--r--	ClassicalEpsilon.v	3629	log plain
-rw-r--r--	ClassicalFacts.v	26470	log plain
-rw-r--r--	ClassicalUniqueChoice.v	3124	log plain
-rw-r--r--	Classical_Pred_Type.v	1963	log plain
-rw-r--r--	Classical_Prop.v	3254	log plain
-rw-r--r--	ConstructiveEpsilon.v	9166	log plain
-rw-r--r--	Decidable.v	5342	log plain
-rw-r--r--	Description.v	900	log plain
-rw-r--r--	Diaconescu.v	9684	log plain
-rw-r--r--	Epsilon.v	2311	log plain
-rw-r--r--	Eqdep.v	1421	log plain
-rw-r--r--	EqdepFacts.v	15644	log plain
-rw-r--r--	Eqdep_dec.v	11604	log plain
-rw-r--r--	ExtensionalFunctionRepresentative.v	1216	log plain
-rw-r--r--	ExtensionalityFacts.v	4503	log plain
-rw-r--r--	FinFun.v	12406	log plain
-rw-r--r--	FunctionalExtensionality.v	8928	log plain
-rw-r--r--	Hurkens.v	22743	log plain
-rw-r--r--	IndefiniteDescription.v	1478	log plain
-rw-r--r--	JMeq.v	3748	log plain
-rw-r--r--	ProofIrrelevance.v	869	log plain
-rw-r--r--	ProofIrrelevanceFacts.v	1965	log plain
-rw-r--r--	PropExtensionality.v	881	log plain
-rw-r--r--	PropExtensionalityFacts.v	3960	log plain
-rw-r--r--	PropFacts.v	1693	log plain
-rw-r--r--	RelationalChoice.v	800	log plain
-rw-r--r--	SetIsType.v	957	log plain
-rw-r--r--	SetoidChoice.v	2241	log plain
-rw-r--r--	WKL.v	9468	log plain
-rw-r--r--	WeakFan.v	3358	log plain