Coq中的一流模塊

Question

任何人都可以給我更多關於Coq中一流模塊的信息嗎？我知道Coq中的模塊不是一流的。我想知道爲什麼？在Coq的未來模塊中有可能是一流的嗎？

非常感謝您

Answer 1

我不能肯定，但據我所知它來自兩個基本點：

1. 勒柯克是保守的。因爲它的一些主要應用程序正在驗證中，Coq大多限於其構造，其語義理解合理。

2. 在依賴類型設置中，第一類模塊相當微妙，並且沒有完全理解。特別是，要在模塊外部看到多少定義的計算/縮減行爲？如果沒有，那麼這已經是可用的，作爲記錄類型。但是如果某些或全部縮減行爲是可見的，那麼很難量化到底有多少，所以很難分析結果模塊的語義。

我不是相關文獻的專家，所以我可能錯了2，但我已經覺得這是基本情況。