Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Library Coq.ZArith.Zlogarithm

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Library Coq.ZArith.Zlogarithm


Chronological Thread 
  • From: Vadim Zaliva <vzaliva AT cmu.edu>
  • To: coq-club AT inria.fr
  • Subject: [Coq-Club] Library Coq.ZArith.Zlogarithm
  • Date: Wed, 1 Apr 2020 11:24:57 -0700
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=vzaliva AT cmu.edu; spf=Pass smtp.mailfrom=vadim.zaliva AT west.cmu.edu; spf=None smtp.helo=postmaster AT mail-io1-f47.google.com
  • Ironport-phdr: 9a23:nV63thC2HDdD7+peHaFGUyQJP3N1i/DPJgcQr6AfoPdwSPvzoMbcNUDSrc9gkEXOFd2Cra4d1qyO6eu5AzZIoc7Y9ixbLNoUD15NoP5VtjJjKfbNMVf8Iv/uYn5yN+V5f3ghwUuGN1NIEt31fVzYry76xzcTHhLiKVg9fbytScbdgMutyu+95YDYbRlWizqhe7NyKwi9oRnMusUMjoZuN6Y8xgHVrndWdOha2H1kKUyOlBr4+su84YRv/itNt/8u7cJMTbn2c6ElRrFEEToqNHw468LsuRTfVwWE+2ESUn8RkhpGAgjF6A/1U5LsuSbkteRzxTeXM9TuQb87RTqt4aFrSAT1iCgcLD427HvXis1rg61Fph+qugFyzJTVYIGRM/p+Y7/dcNYHTmdPQspdSypMCZ66YoASDeQOIPxYopHyqFUOoxWwBhSiCv3zxTJTnHD6wbc33v49HQ3a3gEtGc8FvnTOrNXyMacfSe+6w7PVwjXCavNdxDTy55LMchAgv/GDR697fM3PyUguDQzFilSQqZL/MD6OyusNtnWb4/B+Wu2ylm4qsgd8qSWhyMcrj4nGnIMVylbc+CV/2ok1IMO3RFdnbt6jCpRfqyGaO5FqTcMlRmFlvjsxxL4euZOjYiQG1JAqywTcZvGHaYSE/xPuWeeLLTp3hn9ofq+0iQyo/ki60OL8U9G50FZUoSpBldnBrnUN2AbS6siDU/d9/0Ch1SuW2wDd5exJI1o4laXcK54mzb4wkoQcvV7fES/xnUX6lK6WdkM69ei08+nrfKnqq5uGO4J3igzyKLkil82+DOgiPQUDXXCX+eGm273i+U35Tq9KjvozkqTBrpDVP9kUpq+8AwNP04cs8RK/Dza40NsChnQGIkxKeAmbj4TzJ17OJe34Ae2hjFuxjTdn3+rGMaH5ApXRMnjDl6/scqp6605F0QY80dRf549PBbwaO/LyWkrxtMTCARMjMgy0xfznCNRn2Y8EV2KPGPzRDKSHuliRo+krPuOkZYkPuT+7JeJ2yeTpiCoHkFMceOGb1J8WdnnwSup0KkGYf3PEidIcV2oGo1xtH6TRlFSeXGsLND6JVKUm62RjUdP0PcL4XomoxYe58mK+F5xSaHpBDwnQQ2jlbJnCUPIRLi+eP504y2BWZf2aU4YkkCqWmkri0bM2fOHR52sVuY+xjIEotd2Wrgk78HlPN+rY02yJSDspzGYBRjtz3acm5EIhlRGM1q93h/EeHttWtatE

The library Coq.ZArith.Zlogarithm was deprecated and was removed in 8.11. However, I have proofs depending on it and I could not find some lemmas which were there before. For example: Psize_log_inf, Zlog2_log_inf. 

What is the recommended solution for this?


--
Vadim Zaliva A button for name playback in email signature 
CMU ECE Ph.D. candidate
Mobile/Signal/WhatsApp: +1(510)220-1060





Archive powered by MHonArc 2.6.18.

Top of Page