package info (click to toggle)
coq 8.9.0-1
  • links: PTS, VCS
  • area: main
  • in suites: buster
  • size: 30,604 kB
  • sloc: ml: 192,230; sh: 2,585; python: 2,206; ansic: 1,878; makefile: 818; lisp: 202; xml: 24; sed: 2

Folder: Logic

d .. (parent)
- - rw-r--r-- 4,365 Berardi.v
- - rw-r--r-- 48,510 ChoiceFacts.v
- - rw-r--r-- 816 Classical.v
- - rw-r--r-- 2,207 ClassicalChoice.v
- - rw-r--r-- 3,204 ClassicalDescription.v
- - rw-r--r-- 3,826 ClassicalEpsilon.v
- - rw-r--r-- 26,620 ClassicalFacts.v
- - rw-r--r-- 3,274 ClassicalUniqueChoice.v
- - rw-r--r-- 2,113 Classical_Pred_Type.v
- - rw-r--r-- 3,404 Classical_Prop.v
- - rw-r--r-- 9,316 ConstructiveEpsilon.v
- - rw-r--r-- 5,492 Decidable.v
- - rw-r--r-- 1,050 Description.v
- - rw-r--r-- 9,836 Diaconescu.v
- - rw-r--r-- 2,461 Epsilon.v
- - rw-r--r-- 1,571 Eqdep.v
- - rw-r--r-- 15,794 EqdepFacts.v
- - rw-r--r-- 11,754 Eqdep_dec.v
- - rw-r--r-- 1,366 ExtensionalFunctionRepresentative.v
- - rw-r--r-- 4,653 ExtensionalityFacts.v
- - rw-r--r-- 12,556 FinFun.v
- - rw-r--r-- 9,078 FunctionalExtensionality.v
- - rw-r--r-- 22,893 Hurkens.v
- - rw-r--r-- 1,628 IndefiniteDescription.v
- - rw-r--r-- 3,898 JMeq.v
- - rw-r--r-- 1,019 ProofIrrelevance.v
- - rw-r--r-- 2,115 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,391 SetoidChoice.v
- - rw-r--r-- 9,618 WKL.v
- - rw-r--r-- 3,508 WeakFan.v