The Coq mailing list

[Jean-Francois Monin <jean-francois.monin AT imag.fr>]

The statement of Nat.log2_pow2 is very strange:
why on the hell do they add the precondition add 0 <= nat ???

My 2 cts,
JF

On Thu, Feb 19, 2015 at 11:08:05AM -0500, Abhishek Anand wrote:
>    The official library-docs don't tell the full story :)
>    Coq provides much more powerful ways to search for content.
>    You might want to learn about commands lke SearchAbout, SearchPattern,
>    SearchRewrite, e.t.c :
>    [1]https://coq.inria.fr/distrib/current/refman/command-index.html
>    The commands I used to find the lemma are there in the email itself.
>    If you open CoqIDE and type the following 2 lines, Nat.log2_pow2 will 
> show
>    up in the RHS bottom sub-window
>    Require Export Coq.Numbers.Natural.Peano.NPeano.
>    SearchAbout (log2 (2^?x)).
>    Here is a screenshot:
>    [2]https://dl.dropboxusercontent.com/u/79447152/CoqIDESearch.png
>    Regards,
>    -- Abhishek
>    [3]http://www.cs.cornell.edu/~aa755/
>    On Thu, Feb 19, 2015 at 10:42 AM, Michel Levy
>    
> <[4]michel.levy1948 AT gmail.com>
>  wrote:
> 
>      On 19/02/2015 16:12, Abhishek Anand wrote:
> 
>        It is already there in the standard library:
>        Require Export Coq.Numbers.Natural.Peano.NPeano.
>        SearchAbout (log2 (2^?x)).
>        (*
>        Nat.log2_pow2: forall a : nat, 0 <= a -> log2 (2 ^ a) = a
>        *)
>        -- Abhishek
>        [5]http://www.cs.cornell.edu/~aa755/
> 
>      Thank you really much for your answer.
>      But how did you find it ? I was looking at the "official doc" in
>       
>      
> [6]https://coq.inria.fr/distrib/current/stdlib/Coq.Numbers.Natural.Peano.NPeano.html
>      and I don't find Nat.log2_pow2 on this page or in the web index of the
>      standard library.
> 
>      Sincerely yours.