| Mode | Name | Size | |
|---|---|---|---|
| -rw-r--r-- | Classical_sets.v | 4574 | logplain |
| -rw-r--r-- | Constructive_sets.v | 4950 | logplain |
| -rw-r--r-- | Cpo.v | 4193 | logplain |
| -rw-r--r-- | Ensembles.v | 4006 | logplain |
| -rw-r--r-- | Finite_sets.v | 2966 | logplain |
| -rw-r--r-- | Finite_sets_facts.v | 12150 | logplain |
| -rw-r--r-- | Image.v | 7175 | logplain |
| -rw-r--r-- | Infinite_sets.v | 8853 | logplain |
| -rw-r--r-- | Integers.v | 5323 | logplain |
| -rw-r--r-- | Multiset.v | 5861 | logplain |
| -rw-r--r-- | Partial_Order.v | 3611 | logplain |
| -rw-r--r-- | Permut.v | 2925 | logplain |
| -rw-r--r-- | Powerset.v | 6618 | logplain |
| -rw-r--r-- | Powerset_Classical_facts.v | 11484 | logplain |
| -rw-r--r-- | Powerset_facts.v | 11257 | logplain |
| -rw-r--r-- | Relations_1.v | 2894 | logplain |
| -rw-r--r-- | Relations_1_facts.v | 4032 | logplain |
| -rw-r--r-- | Relations_2.v | 2457 | logplain |
| -rw-r--r-- | Relations_2_facts.v | 5541 | logplain |
| -rw-r--r-- | Relations_3.v | 2656 | logplain |
| -rw-r--r-- | Relations_3_facts.v | 6341 | logplain |
| -rw-r--r-- | Uniset.v | 5519 | logplain |
 |
index : coq | |
| the Coq proof assistant |
| aboutsummaryrefslogtreecommitdiffhomepage |