| Mode | Name | Size | |
|---|---|---|---|
| -rw-r--r-- | Classical_sets.v | 4724 | logplain |
| -rw-r--r-- | Constructive_sets.v | 5100 | logplain |
| -rw-r--r-- | Cpo.v | 4400 | logplain |
| -rw-r--r-- | Ensembles.v | 4156 | logplain |
| -rw-r--r-- | Finite_sets.v | 3116 | logplain |
| -rw-r--r-- | Finite_sets_facts.v | 12300 | logplain |
| -rw-r--r-- | Image.v | 7325 | logplain |
| -rw-r--r-- | Infinite_sets.v | 9010 | logplain |
| -rw-r--r-- | Integers.v | 5473 | logplain |
| -rw-r--r-- | Multiset.v | 6032 | logplain |
| -rw-r--r-- | Partial_Order.v | 3806 | logplain |
| -rw-r--r-- | Permut.v | 3119 | logplain |
| -rw-r--r-- | Powerset.v | 6865 | logplain |
| -rw-r--r-- | Powerset_Classical_facts.v | 11634 | logplain |
| -rw-r--r-- | Powerset_facts.v | 11473 | logplain |
| -rw-r--r-- | Relations_1.v | 3044 | logplain |
| -rw-r--r-- | Relations_1_facts.v | 4219 | logplain |
| -rw-r--r-- | Relations_2.v | 2607 | logplain |
| -rw-r--r-- | Relations_2_facts.v | 5745 | logplain |
| -rw-r--r-- | Relations_3.v | 2806 | logplain |
| -rw-r--r-- | Relations_3_facts.v | 6793 | logplain |
| -rw-r--r-- | Uniset.v | 5741 | logplain |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |