Julin S (Nov 19 2021 at 13:03): Julin S (Nov 19 2021 at 13:03):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.
Karl Palmskog (Nov 19 2021 at 13:13):See all the different log2 in Stdlib here: https://coq.inria.fr/distrib/current/stdlib/index_global_L.html
Julin S (Nov 19 2021 at 13:19):Thanks!
Notification Bot (Nov 19 2021 at 13:19):Ju-sh has marked this topic as resolved.
Alexander Gryzlov (Nov 19 2021 at 16:21):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
Alexander Gryzlov (Nov 19 2021 at 16:22):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
Michael Soegtrop (Nov 19 2021 at 16:34):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).
Michael Soegtrop (Nov 19 2021 at 16:35):(Need to clean this up and move to proper places one day).
Last updated: Sep 30 2023 at 05:01 UTC