K-user mailing list

[Omar Duhaiby <3omarz AT gmail.com>]

rootFloat isn't defined either. Should I import a certain module?

On Mon, Oct 20, 2014 at 4:27 PM, Dwight Guth <dwight.guth AT runtimeverification.com> wrote:

Unfortunately this function was accidentally deleted from the latest master when the floating point support in the framework was updated. I am adding it back in now, but it may be a little bit before it is back in master. In the meantime, feel free to use rootFloat(F:Float, 2)

On Sun, Oct 19, 2014 at 3:02 AM, Omar Duhaiby <3omarz AT gmail.com> wrote:

Hello, I thought sqrtFloat was included in the FLOAT-HOOKS module, which is automatically imported through BUILTIN-HOOKS. But I get a syntax error when I use sqrtFloat. How do I do it?

Thank you

Omar Alzuhaibi

_______________________________________________
k-user mailing list
k-user AT cs.uiuc.edu
http://lists.cs.uiuc.edu/mailman/listinfo/k-user