Logic « theories - coq - the Coq proof assistant

Mode	Name	Size
-rw-r--r--	Berardi.v	4255	log plain
-rw-r--r--	ChoiceFacts.v	26540	log plain
-rw-r--r--	Classical.v	632	log plain
-rw-r--r--	ClassicalChoice.v	2071	log plain
-rw-r--r--	ClassicalDescription.v	3068	log plain
-rw-r--r--	ClassicalEpsilon.v	3614	log plain
-rw-r--r--	ClassicalFacts.v	19491	log plain
-rw-r--r--	ClassicalUniqueChoice.v	2862	log plain
-rw-r--r--	Classical_Pred_Set.v	1602	log plain
-rw-r--r--	Classical_Pred_Type.v	1894	log plain
-rw-r--r--	Classical_Prop.v	3105	log plain
-rw-r--r--	Classical_Type.v	695	log plain
-rw-r--r--	ConstructiveEpsilon.v	5273	log plain
-rw-r--r--	Decidable.v	4997	log plain
-rw-r--r--	DecidableType.v	4459	log plain
-rw-r--r--	DecidableTypeEx.v	3465	log plain
-rw-r--r--	Description.v	914	log plain
-rw-r--r--	Diaconescu.v	9695	log plain
-rw-r--r--	Epsilon.v	2325	log plain
-rw-r--r--	Eqdep.v	1217	log plain
-rw-r--r--	EqdepFacts.v	9516	log plain
-rw-r--r--	Eqdep_dec.v	8701	log plain
-rw-r--r--	FunctionalExtensionality.v	1896	log plain
-rw-r--r--	Hurkens.v	2628	log plain
-rw-r--r--	IndefiniteDescription.v	1492	log plain
-rw-r--r--	JMeq.v	3381	log plain
-rw-r--r--	ProofIrrelevance.v	869	log plain
-rw-r--r--	ProofIrrelevanceFacts.v	1967	log plain
-rw-r--r--	RelationalChoice.v	814	log plain
-rw-r--r--	SetIsType.v	956	log plain
-rwxr-xr-x	intro.tex	247	log plain