导入Agda中的立体Agda模块

Question

我在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文档，我没有看到任何能解决这个问题的地方。有人知道这里发生了什么吗？

Answer 1

立体Agda库只能从立体Agda中使用。错误信息告诉您将源文件更改为使用立体式模式：

{-# OPTIONS --cubical #-}