Alexander Bentkamp

When using an inline annotation in a function that is marked as const, we get the error: ``` cannot call non-const function `hax_lib::assume` in constant functions ```

There is a documentation page for the rust crate hax_lib (https://docs.rs/hax-lib/latest/hax_lib/), but the macros listed there do not contain any explanation about what they do. I imagine this could easily...