package info (click to toggle)
rocq-stdlib 9.0.0-3
  • links: PTS, VCS
  • area: main
  • in suites: experimental
  • size: 11,828 kB
  • sloc: python: 2,928; sh: 444; makefile: 319; javascript: 24; ml: 2

Folder: Logic

d .. (parent)
- - rw-r--r-- 4,434 Adjointification.v
- - rw-r--r-- 4,439 Berardi.v
- - rw-r--r-- 48,907 ChoiceFacts.v
- - rw-r--r-- 839 Classical.v
- - rw-r--r-- 2,247 ClassicalChoice.v
- - rw-r--r-- 3,248 ClassicalDescription.v
- - rw-r--r-- 3,865 ClassicalEpsilon.v
- - rw-r--r-- 30,606 ClassicalFacts.v
- - rw-r--r-- 3,301 ClassicalUniqueChoice.v
- - rw-r--r-- 2,125 Classical_Pred_Type.v
- - rw-r--r-- 3,476 Classical_Prop.v
- - rw-r--r-- 18,031 ConstructiveEpsilon.v
- - rw-r--r-- 6,673 Decidable.v
- - rw-r--r-- 1,062 Description.v
- - rw-r--r-- 10,365 Diaconescu.v
- - rw-r--r-- 2,472 Epsilon.v
- - rw-r--r-- 1,603 Eqdep.v
- - rw-r--r-- 15,617 EqdepFacts.v
- - rw-r--r-- 12,538 Eqdep_dec.v
- - rw-r--r-- 1,366 ExtensionalFunctionRepresentative.v
- - rw-r--r-- 4,674 ExtensionalityFacts.v
- - rw-r--r-- 10,182 FunctionalExtensionality.v
- - rw-r--r-- 5,236 HLevels.v
- - rw-r--r-- 22,984 Hurkens.v
- - rw-r--r-- 1,640 IndefiniteDescription.v
- - rw-r--r-- 4,363 JMeq.v
- - rw-r--r-- 1,086 ProofIrrelevance.v
- - rw-r--r-- 2,132 ProofIrrelevanceFacts.v
- - rw-r--r-- 1,042 PropExtensionality.v
- - rw-r--r-- 4,109 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,452 SetoidChoice.v
- - rw-r--r-- 1,342 StrictProp.v
- - rw-r--r-- 9,792 WKL.v
- - rw-r--r-- 3,479 WeakFan.v