We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
Moved functions to code snippets
Reverted rename
Changed title and summary to reflect that this is no longer a draft
Removed duplicate word
Added note regarding trailing zeros in the significand of floating-point constants.
Updated constant syntax, cleaned up links, and reworded some sentences.
Removed reference to to_fp function that accepts int; this function does not exist.
Updated Draft floating point Boogie language extension (markdown)
fixed argument in "Type conversion" example and added back in a section on the ":rm" attribute.
Fixed number of arguments in sqrt function example.
Fixed various errors (incorrect ordering of "builtin" function arguments, undeclared variables in code examples, formatting issues) and rewrote parts of some sections.
Fixed return type of fp.min and fp.max operators.
fp must be used declaring constants instead of float when declaring constants so that the compliter can differentiate between variable and constant declaration.
Undoing previous change (which was incorrect)
Using a bitvector to declare a constant defined with the float<exp, sig> (value) syntax shouldn't require a bitvector in the value field
Added commas for data delimination
Created initial draft of the body of the wiki
Add stub for type conversion
Stub out draft document.