Agda是一种依赖类型的全功能编程语言和证明助手。
未能解决约束：(k ≤ 5) x (k * 2 ≡ 5)。我怎样才能做到这一点？
我是 agda 的新手，正在尝试证明 5 是质数:)。 我现在试图否认 2 是 5 的约数。我有： p1 : k * 2 == 5 p2：k≤5 我现在希望模式匹配如下： 案例（p2 ...
在 Agda 中，如何定义与以下内容等效的参数化模块？ data Sig : 设置 ℓ 其中 ■ ：排序→签名 ν : Sig → Sig module SortedABT {ℓ}（排序：设置ℓ）（操作：排序→设置ℓ）（sig：...
在 PLFA 中，他们定义了逆关系： inv-z≤n : ∀ {m : ℕ} → m ≤ 0 ---------------------- → m ≠ 0 然后断言： inv-z≤n z≤n = refl 我的问题...
我在 PLFA 之后的 Agda 中尝试了一下证明，特别是 monus 运算符。 ——莫努斯 _∸_ : ℕ → ℕ → ℕ m ∸ 零 = m 零 ∸ suc (m) = 零 suc (n) ∸ suc(m) = n ∸ m 还有我的问题
当我尝试从 Agda 中的编程语言基础加载此示例时，它失败了： 模块测试在哪里 导入 Relation.Binary.PropositionalEquality 作为 Eq 使用 (_≡_; refl) 打开 Eq 开方程 ==-
Agda：为什么编译器在数据定义中要求 Set_1，而不是 Set？
尝试在Agda 2.6.4中定义一个简单的集合积： 模块布尔值在哪里 使用 (id ; const ; _∘_ ; _$_ ) 打开导入函数 打开导入 Agda.Primitive 多变的 一个等级 A B C：设置 数据_×_：...
Agda 错误：使用 --guardedness 标志从不支持的模块导入模块 IO
我这个例子取自 Agda 文档 模块 hello-world-prog 其中 打开导入IO 主要：主要 main = run（putStrLn“你好，世界！”） 但是当我运行 Ctrl+c、Ctrl+x、Ctrl...
我有以下 Agda 文件（名为 hello-world.agda），直接取自 Agda 文档： 模块 hello-world 其中 模块 B 其中 f : 纳特 → 纳特 f n = suc n g : 纳特 → 纳特 → 纳特...
我想证明 ∀ {ℓ} {A B C D : 集合 ℓ} → (A → B) ≡ (C → D) → A ≡ C （与密码域类似）。 如果我有一个返回函数类型域的函数域，我可以写出证明......
练习*-assoc（推荐）{#times-assoc} 显示乘法是结合律的，即 (m * n) * p == m * (n * p) 对于所有自然数 m、n 和 p。 *-关联 : ∀ (m n p : ℕ) → (m * n) * p ≡ m * (n * ...
我正在研究涉及 Agda 中 scanr 函数的证明，并且在分支推理方面遇到了困难。证明看起来很简单，但实施起来却很棘手。他...
agda：如何证明Agda中涉及分支推理的`scanr`基本属性？
我正在研究涉及 Agda 中 scanr 函数的证明，并且在分支推理方面遇到了困难。证明看起来很简单，但实施起来却很棘手。他...
我目前正在为此项目编写以下不完整的函数： 扩展 : ∀ o asc (s : CSet (suck) o) → SC asc → SC (add s asc) 扩展 0 asc s 重写 l≡0 s Eq.refl = 限制（添加（
我一直在尝试“移植”一些在 Isabelle 中形式化的命令式语言（IMP2）：https://www.isa-afp.org/sessions/imp2/#Semantics.html 到阿格达。 首先，这是一些初步翻译...
`agda`：如何指定方程推理中的步骤是通过函数的定义来实现的？
我是 agda 的新手。当我进行等式推理时，如何指定特定步骤是通过函数的定义来实现的？ 例如，采用以下自然数定义： 打开导入
Agda 模式（用于帮助发现证明的工具）与 agda-setup 命令初始化的程序一起不起作用。我已经通过 sudo 使用尝试过此操作并遇到相同的错误。 ...
所以这是我在家庭作业中遇到的问题，我必须证明 bool 不等于 top，而且我必须使用一个重新定义的等号。 模块 TranspEq 其中 打开导入 Agda.Prim...
我正在尝试编写 Agda 程序，并在模块导入部分中查找包以供参考。 据我所知 ≣ 是由 \=== 产生的。 Greping agda-library 和 agda-stdlib 项目...
我在 Agda 中创建了一个递归数据类型“Positive”。我使用这种数据类型来索引一些树。 在这些树上，我试图证明对某些索引 q 的设置操作不会影响 get 操作...
我有一个记录类型，在 Agda 中调用 if Foo。我可以通过生成字符串表示形式（显示 foo）并对结果字符串进行排序来对其进行排序。我有一个亲戚，请称呼它<=Foo, for comparing...