| Mode | Name | Size | |
|---|---|---|---|
| -rw-r--r-- | add.v | 2059 | logplain |
| -rw-r--r-- | classify.v | 971 | logplain |
| -rw-r--r-- | coq_env_double_array.v | 307 | logplain |
| -rw-r--r-- | div.v | 2504 | logplain |
| -rw-r--r-- | double_rounding.v | 1225 | logplain |
| -rw-r--r-- | frexp.v | 1550 | logplain |
| -rw-r--r-- | mul.v | 2533 | logplain |
| -rw-r--r-- | next_up_down.v | 5834 | logplain |
| -rw-r--r-- | normfr_mantissa.v | 1001 | logplain |
| -rw-r--r-- | spec_conv.v | 1660 | logplain |
| -rw-r--r-- | sqrt.v | 1415 | logplain |
| -rw-r--r-- | sub.v | 1871 | logplain |
| -rw-r--r-- | valid_binary_conv.v | 1711 | logplain |
| -rw-r--r-- | zero.v | 185 | logplain |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |