Is there a built-in function to do logarithm to base 2 with coq?
Found https://coq.inria.fr/library/Coq.Numbers.NatInt.NZLog.html but couldn't figure how to use it.
See all the different
log2 in Stdlib here: https://coq.inria.fr/distrib/current/stdlib/index_global_L.html
Ju-sh has marked this topic as resolved.
I've been looking for this in Mathcomp recently for my FAV port, found some stuff in https://github.com/thery/mathcomp-extra/blob/master/more_thm.v
So I just copied it to my prelude and added a few lemmas of my own: https://github.com/clayrat/fav-ssr/blob/trunk/src/prelude.v#L103
There are also a floor and ceil log2 function for positives at the beginning of this file : (https://github.com/coq/coq/blob/master/theories/Reals/Cauchy/QExtra.v).
(Need to clean this up and move to proper places one day).
Last updated: Jan 29 2023 at 01:02 UTC