我在 Emacs 模式下使用 agda。我正在嘗試啟動一個依賴立方庫的專案。我想匯入模塊 Cubical.Core.Everything。我只寫了以下內容
{-# OPTIONS --without-K #-}
open import Cubical.Core.Everything
當我嘗試加載檔案時，我收到以下錯誤
/home/rymndbkr/myHoTT/Agda/intro.agda:3,1-36
Importing module Cubical.Core.Everything using the
--cubical/--erased-cubical flag from a module which does not.
when scope checking the declaration
open import Cubical.Core.Everything
/home/rymndbkr/myHoTT/Agda/intro.agda:3,1-36
Importing module Cubical.Core.Everything using the --two-level flag
from a module which does not.
when scope checking the declaration
open import Cubical.Core.Everything
我已經閱讀了相關的 agda 檔案，但沒有看到任何解決此問題的內容。有誰知道這里發生了什么？
uj5u.com熱心網友回復：
Cubical Agda 庫只能從 Cubical Agda 使用。錯誤訊息告訴您更改源檔案以使用 Cubical 模式：
{-# OPTIONS --cubical #-}
轉載請註明出處，本文鏈接：https://www.uj5u.com/net/536815.html
標籤：阿格达