| Mode | Name | Size | |
|---|---|---|---|
| -rw-r--r-- | add.v | 495 | logplain |
| -rw-r--r-- | addc.v | 552 | logplain |
| -rw-r--r-- | addcarryc.v | 612 | logplain |
| -rw-r--r-- | addmuldiv.v | 426 | logplain |
| -rw-r--r-- | compare.v | 702 | logplain |
| -rw-r--r-- | div.v | 422 | logplain |
| -rw-r--r-- | diveucl.v | 530 | logplain |
| -rw-r--r-- | diveucl_21.v | 1501 | logplain |
| -rw-r--r-- | eqb.v | 551 | logplain |
| -rw-r--r-- | head0.v | 711 | logplain |
| -rw-r--r-- | isint.v | 1840 | logplain |
| -rw-r--r-- | land.v | 1234 | logplain |
| -rw-r--r-- | leb.v | 763 | logplain |
| -rw-r--r-- | lor.v | 1470 | logplain |
| -rw-r--r-- | lsl.v | 819 | logplain |
| -rw-r--r-- | lsr.v | 837 | logplain |
| -rw-r--r-- | ltb.v | 758 | logplain |
| -rw-r--r-- | lxor.v | 1360 | logplain |
| -rw-r--r-- | mod.v | 438 | logplain |
| -rw-r--r-- | mul.v | 620 | logplain |
| -rw-r--r-- | mulc.v | 827 | logplain |
| -rw-r--r-- | reduction.v | 683 | logplain |
| -rw-r--r-- | sub.v | 548 | logplain |
| -rw-r--r-- | subc.v | 606 | logplain |
| -rw-r--r-- | subcarryc.v | 666 | logplain |
| -rw-r--r-- | tail0.v | 711 | logplain |
| -rw-r--r-- | unsigned.v | 559 | logplain |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |