Stream: Coq users

Topic: ✔ binary logarithm on nat


view this post on Zulip Pierre Rousselin (Dec 05 2022 at 08:11):

Thank you @Huỳnh Trần Khanh for the nice trick (and the cool interpretation of the second variable as fuel).
Thank you @Guillaume Melquiond for the explanation. Maybe it could be possible to let n0 appear in the definition, as printed by coq (it's already different from what I wrote) ?

view this post on Zulip Notification Bot (Dec 05 2022 at 08:12):

Pierre Rousselin has marked this topic as resolved.


Last updated: Feb 08 2023 at 23:03 UTC