| Mode | Name | Size | |
|---|---|---|---|
| -rw-r--r-- | Classical_sets.v | 4661 | logplain |
| -rw-r--r-- | Constructive_sets.v | 5040 | logplain |
| -rw-r--r-- | Cpo.v | 4203 | logplain |
| -rw-r--r-- | Ensembles.v | 4030 | logplain |
| -rw-r--r-- | Finite_sets.v | 3004 | logplain |
| -rw-r--r-- | Finite_sets_facts.v | 12267 | logplain |
| -rw-r--r-- | Image.v | 7237 | logplain |
| -rw-r--r-- | Infinite_sets.v | 8920 | logplain |
| -rw-r--r-- | Integers.v | 5432 | logplain |
| -rw-r--r-- | Multiset.v | 5724 | logplain |
| -rw-r--r-- | Partial_Order.v | 3702 | logplain |
| -rw-r--r-- | Permut.v | 2938 | logplain |
| -rw-r--r-- | Powerset.v | 6779 | logplain |
| -rw-r--r-- | Powerset_Classical_facts.v | 11699 | logplain |
| -rw-r--r-- | Powerset_facts.v | 8651 | logplain |
| -rw-r--r-- | Relations_1.v | 2915 | 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 | 5602 | logplain |
| -rw-r--r-- | Relations_3.v | 2694 | logplain |
| -rw-r--r-- | Relations_3_facts.v | 6458 | logplain |
| -rw-r--r-- | Uniset.v | 5740 | logplain |
| -rwxr-xr-x | intro.tex | 733 | logplain |
 |
index : coq | |
| the Coq proof assistant |
| aboutsummaryrefslogtreecommitdiffhomepage |