Folder: Logic

package info (click to toggle)

coq-doc 8.20.0-2

links: PTS, VCS
area: non-free
in suites: forky, sid, trixie
size: 46,708 kB
sloc: ml: 234,429; sh: 4,686; python: 3,359; ansic: 2,644; makefile: 842; lisp: 172; javascript: 87; xml: 24; sed: 2

			.. (parent)
-	rw-r--r--	4,434	Adjointification.v
-	rw-r--r--	4,440	Berardi.v
-	rw-r--r--	48,835	ChoiceFacts.v
-	rw-r--r--	816	Classical.v
-	rw-r--r--	2,211	ClassicalChoice.v
-	rw-r--r--	3,212	ClassicalDescription.v
-	rw-r--r--	3,842	ClassicalEpsilon.v
-	rw-r--r--	27,366	ClassicalFacts.v
-	rw-r--r--	3,277	ClassicalUniqueChoice.v
-	rw-r--r--	2,113	Classical_Pred_Type.v
-	rw-r--r--	3,452	Classical_Prop.v
-	rw-r--r--	18,027	ConstructiveEpsilon.v
-	rw-r--r--	6,673	Decidable.v
-	rw-r--r--	1,050	Description.v
-	rw-r--r--	10,354	Diaconescu.v
-	rw-r--r--	2,461	Epsilon.v
-	rw-r--r--	1,591	Eqdep.v
-	rw-r--r--	15,617	EqdepFacts.v
-	rw-r--r--	11,671	Eqdep_dec.v
-	rw-r--r--	1,366	ExtensionalFunctionRepresentative.v
-	rw-r--r--	4,677	ExtensionalityFacts.v
-	rw-r--r--	13,371	FinFun.v
-	rw-r--r--	10,185	FunctionalExtensionality.v
-	rw-r--r--	5,225	HLevels.v
-	rw-r--r--	22,985	Hurkens.v
-	rw-r--r--	1,628	IndefiniteDescription.v
-	rw-r--r--	4,341	JMeq.v
-	rw-r--r--	1,074	ProofIrrelevance.v
-	rw-r--r--	2,120	ProofIrrelevanceFacts.v
-	rw-r--r--	1,031	PropExtensionality.v
-	rw-r--r--	4,110	PropExtensionalityFacts.v
-	rw-r--r--	1,843	PropFacts.v
-	rw-r--r--	950	RelationalChoice.v
-	rw-r--r--	1,107	SetIsType.v
-	rw-r--r--	2,392	SetoidChoice.v
-	rw-r--r--	1,342	StrictProp.v
-	rw-r--r--	9,751	WKL.v
-	rw-r--r--	3,512	WeakFan.v