我正在研究依賴模式匹配在 agda 中的作業原理。如果我能看到 .agda 檔案的任意源代碼的詳細核心術語（https://github.com/agda/agda/blob/master/src/full/Agda/Syntax/Internal.hs#L202），它將是對我真的很有幫助。
但是，agda cli 似乎沒有為這種用法提供任何選項。有沒有？
uj5u.com熱心網友回復：
根據您想要的詳細程度，您可以嘗試三種選擇，但它們都不是完美的：
如果你只想查看 Agda 插入了哪些隱式引數，你可以啟用標志
--show-implicit和--show-irrelevant，通過在檔案底部添加你想要檢查的術語創建一個新洞，使用_ = {! yourTerm !}重新加載檔案C-c C-l，然后C-u C-c C-m按孔內的游標。[寫出來讓我意識到應該有一種更簡單的方法來做到這一點。]如果你想檢查并可能操作 Agda 術語的完整 AST，你可以使用反射 API ( https://agda.readthedocs.io/en/v2.6.2.1/language/reflection.html ) 來實作。特別是，您可以使用
quoteTerm原語獲取任意 Agda 項的反射語法。最后，如果您需要更多資訊，您可以查看 Agda 本身的源代碼并啟用除錯標志以列印您想要的資訊。請注意，不能保證此除錯資訊有用甚至可讀，因為它旨在供開發人員使用。
{-# OPTIONS -v tc.cc:12 #-}話雖如此，您可以通過在檔案頂部添加模式匹配來列印從定義生成的案例樹。在 Emacs 中，此除錯資訊將在一個名為的單獨緩沖區中結束*Agda debug*（您必須在加載 .agda 檔案后手動打開該緩沖區）。
轉載請註明出處，本文鏈接：https://www.uj5u.com/net/536818.html
標籤：阿格达
上一篇：如何撰寫帶有兩個引數的型別簽名？
下一篇：Bash替換從命令末尾傳遞