Re: [isabelle] Code equations for "power"
>> Lastly, I was wondering whether there was something like "divmod" in Isabelle, i.e. an
>> operation that returns both the quotient and the remainder, since most languages have a
>> corresponding operation that is more efficient than computing the two separately.
> There are various specialised divmod constants in HOL, e.g., divmod_integer, semiring_numeral_div_class.divmod and Divides.divmod_nat, but no systematic, algebraic treatment.
If you care about efficiency, you might also have a look at improved code equations for divmod, e.g., under
for Isabelle 2015
for Isabelle 2016-RC0.
This archive was generated by a fusion of
Pipermail (Mailman edition) and