| Mode | Name | Size | |
|---|---|---|---|
| -rw-r--r-- | Disjoint_Union.v | 1716 | logplain |
| -rw-r--r-- | Inclusion.v | 1163 | logplain |
| -rw-r--r-- | Inverse_Image.v | 1873 | logplain |
| -rw-r--r-- | Lexicographic_Exponentiation.v | 8469 | logplain |
| -rw-r--r-- | Lexicographic_Product.v | 4504 | logplain |
| -rw-r--r-- | Transitive_Closure.v | 1599 | logplain |
| -rw-r--r-- | Union.v | 2462 | logplain |
| -rw-r--r-- | Well_Ordering.v | 2181 | logplain |
| -rw-r--r-- | Wellfounded.v | 934 | logplain |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |