Coq循環模塊使用示例

Question

我想模擬Coq中的32位整數運算。我認爲循環模塊最適合這個。但是我想要弄清楚如何使用這個模塊有一些困難。你能否給我提供一些例子說明如何使用它？其他數字模塊（如Integer，Natural或Rational）的示例也非常有用。

Answer 1

允許我不回答你的問題：32位整數算術已經在Coq生態系統中被模擬爲死亡。

您可能想看看CompCert的Integer.v或x86proved的bits。後一個庫已經被我的學生Arthur Blot here重新打包，並將它擴展爲OCaml整數的trustworthy extraction。它應該儘快登陸coq-opam。