Sail has built-in support for 2 ^, and this is the only exponent we use so there's no need for the more generic int_power. Additionally the type of int_power is both way looser than 2 ^ (which is understood at the type level), and actually wrong, e.g. it will let you do 3 ^ -1 and give the result as 3.
Sail has built-in support for
2 ^
, and this is the only exponent we use so there's no need for the more genericint_power
. Additionally the type ofint_power
is both way looser than2 ^
(which is understood at the type level), and actually wrong, e.g. it will let you do3 ^ -1
and give the result as 3.Note I had to add spaces because this was required until a very recent Sail version - see https://github.com/rems-project/sail/issues/657