Mode | Name | Size | |
---|---|---|---|
-rw-r--r-- | Berardi.v | 4306 | logplain |
-rw-r--r-- | ChoiceFacts.v | 4872 | logplain |
-rwxr-xr-x | Classical.v | 687 | logplain |
-rw-r--r-- | ClassicalChoice.v | 1315 | logplain |
-rw-r--r-- | ClassicalDescription.v | 2674 | logplain |
-rw-r--r-- | ClassicalFacts.v | 7501 | logplain |
-rwxr-xr-x | Classical_Pred_Set.v | 1965 | logplain |
-rwxr-xr-x | Classical_Pred_Type.v | 1969 | logplain |
-rwxr-xr-x | Classical_Prop.v | 2311 | logplain |
-rwxr-xr-x | Classical_Type.v | 701 | logplain |
-rw-r--r-- | Decidable.v | 1946 | logplain |
-rw-r--r-- | Diaconescu.v | 4350 | logplain |
-rwxr-xr-x | Eqdep.v | 5343 | logplain |
-rw-r--r-- | Eqdep_dec.v | 3833 | logplain |
-rw-r--r-- | Hurkens.v | 2621 | logplain |
-rw-r--r-- | JMeq.v | 2166 | logplain |
-rw-r--r-- | ProofIrrelevance.v | 3969 | logplain |
-rw-r--r-- | RelationalChoice.v | 940 | logplain |
-rwxr-xr-x | intro.tex | 247 | logplain |