Folder: Logic

package info (click to toggle)

coq-doc 8.4pl4-1

			.. (parent)
-	rw-r--r--	4,185	Berardi.v
-	rw-r--r--	28,445	ChoiceFacts.v
-	rw-r--r--	666	Classical.v
-	rw-r--r--	2,057	ClassicalChoice.v
-	rw-r--r--	3,054	ClassicalDescription.v
-	rw-r--r--	3,629	ClassicalEpsilon.v
-	rw-r--r--	19,381	ClassicalFacts.v
-	rw-r--r--	3,123	ClassicalUniqueChoice.v
-	rw-r--r--	1,680	Classical_Pred_Set.v
-	rw-r--r--	1,963	Classical_Pred_Type.v
-	rw-r--r--	3,270	Classical_Prop.v
-	rw-r--r--	681	Classical_Type.v
-	rw-r--r--	9,205	ConstructiveEpsilon.v
-	rw-r--r--	4,981	Decidable.v
-	rw-r--r--	900	Description.v
-	rw-r--r--	9,655	Diaconescu.v
-	rw-r--r--	2,311	Epsilon.v
-	rw-r--r--	1,425	Eqdep.v
-	rw-r--r--	11,958	EqdepFacts.v
-	rw-r--r--	8,930	Eqdep_dec.v
-	rw-r--r--	4,503	ExtensionalityFacts.v
-	rw-r--r--	1,868	FunctionalExtensionality.v
-	rw-r--r--	2,612	Hurkens.v
-	rw-r--r--	1,478	IndefiniteDescription.v
-	rw-r--r--	3,684	JMeq.v
-	rw-r--r--	869	ProofIrrelevance.v
-	rw-r--r--	1,964	ProofIrrelevanceFacts.v
-	rw-r--r--	800	RelationalChoice.v
-	rw-r--r--	957	SetIsType.v
-	rwxr-xr-x	247	intro.tex
-	rw-r--r--	488	vo.itarget