| Mode | Name | Size | |
|---|---|---|---|
| -rw-r--r-- | .cvsignore | 5 | logplain |
| -rwxr-xr-x | Classical_sets.v | 4536 | logplain |
| -rwxr-xr-x | Constructive_sets.v | 5101 | logplain |
| -rwxr-xr-x | Cpo.v | 4199 | logplain |
| -rwxr-xr-x | Ensembles.v | 4003 | logplain |
| -rwxr-xr-x | Finite_sets.v | 2936 | logplain |
| -rwxr-xr-x | Finite_sets_facts.v | 11394 | logplain |
| -rwxr-xr-x | Image.v | 6797 | logplain |
| -rwxr-xr-x | Infinite_sets.v | 8311 | logplain |
| -rwxr-xr-x | Integers.v | 5253 | logplain |
| -rwxr-xr-x | Multiset.v | 5351 | logplain |
| -rwxr-xr-x | Partial_Order.v | 3531 | logplain |
| -rwxr-xr-x | Permut.v | 2758 | logplain |
| -rwxr-xr-x | Powerset.v | 6772 | logplain |
| -rwxr-xr-x | Powerset_Classical_facts.v | 10805 | logplain |
| -rwxr-xr-x | Powerset_facts.v | 8228 | logplain |
| -rwxr-xr-x | Relations_1.v | 2944 | logplain |
| -rwxr-xr-x | Relations_1_facts.v | 4110 | logplain |
| -rwxr-xr-x | Relations_2.v | 2498 | logplain |
| -rwxr-xr-x | Relations_2_facts.v | 5612 | logplain |
| -rwxr-xr-x | Relations_3.v | 2721 | logplain |
| -rwxr-xr-x | Relations_3_facts.v | 6451 | logplain |
| -rw-r--r-- | Uniset.v | 5741 | logplain |
| -rwxr-xr-x | intro.tex | 733 | logplain |
 |
index : coq | |
| the Coq proof assistant |
| aboutsummaryrefslogtreecommitdiffhomepage |