coq-club AT inria.fr

Subject: The Coq mailing list

List archive

From: Vincent Laporte <vincent.laporte AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Library Coq.ZArith.Zlogarithm
Date: Thu, 2 Apr 2020 11:43:19 +0200
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=vincent.laporte AT gmail.com; spf=Pass smtp.mailfrom=vincent.laporte AT gmail.com; spf=None smtp.helo=postmaster AT mail-wr1-f54.google.com
Ironport-phdr: 9a23:VdgH4RywvaVCWinXCy+O+j09IxM/srCxBDY+r6Qd0u0eIJqq85mqBkHD//Il1AaPBtqLra8cw8Pt8IneGkU4qa6bt34DdJEeHzQksu4x2zIaPcieFEfgJ+TrZSFpVO5LVVti4m3peRMNQJW2UXSJ/Sb3tWJaWkindFk9GuOgEYnLys+zyuqa+pvJYgwOiiDuT6l1KUCIrAPau88Kya9rMqEr1haB9mVJfe9bw38uIVuLmAzg6++/+Zdi92JbvPd3pJ0IarnzY6ltFe8QNz8hKW1guZWy6UvzCDCX735ZaV041wJSClGcvh7/V5b19CD9s7glgXTIDYjNVbkxHA+aweJrRRvv0npVMjc49CTIkJU1gv8H5h2moBN7zsjfZ4THbKMvLJOYRssTQC96ZugUUiVABo2maI5WVrgOOO9Zq8/2oF5c9BY=

Hello,

You can have a look at this commit:
https://github.com/AbsInt/CompCert/pull/286/commits/182afce7114ebf870fe6eabd1dc53bd8f7fae50a

It gives you a lemma linking Pos.size and Z.log2.

Cheers,
--
Vincent.

[Coq-Club] Library Coq.ZArith.Zlogarithm, Vadim Zaliva, 04/01/2020
- Re: [Coq-Club] Library Coq.ZArith.Zlogarithm, Vincent Laporte, 04/02/2020