| Mode | Name | Size | |
|---|---|---|---|
| -rw-r--r-- | add.v | 2534 | logplain |
| -rw-r--r-- | classify.v | 1452 | logplain |
| -rw-r--r-- | compare.v | 17279 | logplain |
| -rw-r--r-- | coq_env_double_array.v | 307 | logplain |
| -rw-r--r-- | div.v | 3380 | logplain |
| -rw-r--r-- | double_rounding.v | 1660 | logplain |
| -rw-r--r-- | frexp.v | 2369 | logplain |
| -rwxr-xr-x | gen_compare.sh | 1695 | logplain |
| -rw-r--r-- | ldexp.v | 937 | logplain |
| -rw-r--r-- | mul.v | 3415 | logplain |
| -rw-r--r-- | next_up_down.v | 11528 | logplain |
| -rw-r--r-- | normfr_mantissa.v | 1483 | logplain |
| -rw-r--r-- | spec_conv.v | 2396 | logplain |
| -rw-r--r-- | sqrt.v | 1755 | logplain |
| -rw-r--r-- | sub.v | 2426 | logplain |
| -rw-r--r-- | syntax.v | 374 | logplain |
| -rw-r--r-- | valid_binary_conv.v | 2461 | logplain |
| -rw-r--r-- | zero.v | 185 | logplain |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |