| Mode | Name | Size | |
|---|---|---|---|
| -rw-r--r-- | 1338.v-disabled | 332 | logplain |
| -rw-r--r-- | 1501.v | 2587 | logplain |
| -rw-r--r-- | 1596.v | 7383 | logplain |
| -rw-r--r-- | 1671.v | 322 | logplain |
| -rw-r--r-- | 1773.v | 192 | logplain |
| -rw-r--r-- | 1811.v | 200 | logplain |
| -rw-r--r-- | 2310.v | 642 | logplain |
| -rw-r--r-- | 3230.v | 372 | logplain |
| -rw-r--r-- | 3263.v | 9733 | logplain |
| -rw-r--r-- | 3277.v | 188 | logplain |
| -rw-r--r-- | 3278.v | 633 | logplain |
| -rw-r--r-- | 3283.v | 1019 | logplain |
| -rw-r--r-- | 3295.v | 3057 | logplain |
| -rw-r--r-- | 3298.v | 508 | logplain |
| -rw-r--r-- | 3304.v | 203 | logplain |
| -rw-r--r-- | 3309.v | 11789 | logplain |
| -rw-r--r-- | 3311.v | 337 | logplain |
| -rw-r--r-- | 3312.v | 185 | logplain |
| -rw-r--r-- | 3326.v | 384 | logplain |
| -rw-r--r-- | 3337.v | 107 | logplain |
| -rw-r--r-- | 3343.v | 1296 | logplain |
| -rw-r--r-- | 3345.v | 5372 | logplain |
| -rw-r--r-- | 3357.v | 321 | logplain |
| -rw-r--r-- | 3363.v | 479 | logplain |
| -rw-r--r-- | 3370.v | 341 | logplain |
| -rw-r--r-- | 3383.v | 506 | logplain |
| -rw-r--r-- | 3388.v | 1295 | logplain |
| -rw-r--r-- | 3395.v | 9693 | logplain |
| -rw-r--r-- | 743.v | 218 | logplain |
| -rw-r--r-- | HoTT_coq_077.v | 1103 | logplain |
| -rw-r--r-- | HoTT_coq_083.v | 589 | logplain |
| -rw-r--r-- | HoTT_coq_106.v | 2002 | logplain |
| -rw-r--r-- | HoTT_coq_120.v | 5392 | logplain |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |