| Mode | Name | Size | |
|---|---|---|---|
| -rw-r--r-- | Classical_sets.v | 4543 | logplain |
| -rw-r--r-- | Constructive_sets.v | 5108 | logplain |
| -rw-r--r-- | Cpo.v | 4206 | logplain |
| -rw-r--r-- | Ensembles.v | 4010 | logplain |
| -rw-r--r-- | Finite_sets.v | 2943 | logplain |
| -rw-r--r-- | Finite_sets_facts.v | 11401 | logplain |
| -rw-r--r-- | Image.v | 6804 | logplain |
| -rw-r--r-- | Infinite_sets.v | 8318 | logplain |
| -rw-r--r-- | Integers.v | 5260 | logplain |
| -rw-r--r-- | Multiset.v | 5358 | logplain |
| -rw-r--r-- | Partial_Order.v | 3538 | logplain |
| -rw-r--r-- | Permut.v | 2765 | logplain |
| -rw-r--r-- | Powerset.v | 6779 | logplain |
| -rw-r--r-- | Powerset_Classical_facts.v | 10812 | logplain |
| -rw-r--r-- | Powerset_facts.v | 8235 | logplain |
| -rw-r--r-- | Relations_1.v | 2951 | logplain |
| -rw-r--r-- | Relations_1_facts.v | 4117 | logplain |
| -rw-r--r-- | Relations_2.v | 2486 | logplain |
| -rw-r--r-- | Relations_2_facts.v | 5619 | logplain |
| -rw-r--r-- | Relations_3.v | 2718 | logplain |
| -rw-r--r-- | Relations_3_facts.v | 6458 | logplain |
| -rw-r--r-- | Uniset.v | 5748 | logplain |
| -rwxr-xr-x | intro.tex | 733 | logplain |
 |
index : coq | |
| the Coq proof assistant |
| aboutsummaryrefslogtreecommitdiffhomepage |