Re: [isabelle] Code equations for "power"

Dear Manuel,

>> 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

and under

for Isabelle 2016-RC0.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.