agda 相关问题

Agda 未解决的元数据

我创建了一个树数据类型。以及一个应该从中检索值的 get 函数。我现在想创建一个证明，从空树中检索任何值都将返回“无”。 （我

使用标准库对 Agda 中的对/列表进行字典顺序排序

Agda 标准库包含一些模块 Relation.Binary.*.(Non)StrictLex （目前仅适用于 Product 和 List）。我们可以使用这些模块轻松构造一个实例，例如，

立方 Agda 包含顺序

我快要完成在 Cubical Agda 中定义包含顺序了，但我一直在证明第二个投影对于依赖对来说是相等的。如果有人可以填补这个漏洞，我将不胜感激......

如何处理Cubical Agda中的非终止错误

我使用的是 M 型的通常共归纳定义，定义如下。 记录 M (S : 设置) (Q : S → 设置) : 设置在哪里 共感的 构造函数sup-M 场地 形状：S 位置 : Q 形状 → M ...

How to shuffle a list i agda?

我想在 agda 中随机洗牌。 我考虑过从头开始随机取 n 个元素并将它们添加到末尾，但我无法通过这种方法使随机部分起作用......

每次我尝试使用箭头键浏览时，VSCode 都出现“未找到命令‘agda-mode.input-symbol[BrowseLeft]’”错误

我不知道发生了什么。我在一个窗口中做一些 Agda 工作，而在另一个窗口中有一个 C 项目。重新启动 VS Code 以处理 C 项目，现在每次我尝试使用箭头键时，我都会得到

Agda notNotExcludedMiddle

有人能解释一下如何从以下 Agda 表达式中推导出双重否定的排中律吗？ data 或 (a b : Set) : 设置在哪里 Inl : a -> 或 a b Inr : b -> 或 a b 或大小写：...

Agda：在求解 divison 属性时未能求解以下约束

我有以下代码： 模块 div 在哪里 使用 (ℕ; zero; suc; _+_) 打开导入 Data.Nat 使用 (+-assoc) 打开导入 Data.Nat.Properties 打开导入 Relation.Binary.PropositionalEquality 使用 (_≡_; r...

如何证明荒谬模式的两个应用在 Cubical Agda 中产生相同的结果？

重范畴论（agda-categories）相关问题。 我试图定义一个自然变换并证明它的自然性广场通勤。本质上，我遇到的错误是两个“

覆盖二元自然型的高级归纳类型。

我之前的一个问题的答案指出，在Cubical Agda (v2.6.1, Cubical repo版本acabbd9)中，给定一个归纳类型，我们应该通过递归在数据类型上定义一个关系，然后......

无法解析左侧(m+1)*n。

我刚开始学习Agda，读的是《Agda编程语言基础》。就在第一章有一个乘法的定义，其中一种情况是(suc m) * n = n + (m * n)......。

利用平等关系证明定理：∀[ x ]∀[ y ] (¬ Eq x y →¬ Eq (f x) (f y))

我想用Agda解决以下一阶逻辑问题：问题：{A B : Set}。{f : A → B} → inj f → ∀[ x ] ∀[ y ] (¬ Eq x y →¬ Eq (f x) (f y))利用下面的定义 ...

利用平等关系证明定理：∀[ x ]∀[ y ] (¬ Eq x y →¬ Eq (f x) (f y))

我想用Agda解决以下一阶逻辑问题：问题：{A B : Set}。{f : A → B} → inj f → ∀[ x ] ∀[ y ] (¬ Eq x y →¬ Eq (f x) (f y))利用下面的定义 ...

构建基本Agda函数时克服定义平等问题

我想用agda写一个反向向量函数，遇到了以下的绊脚石 Goal: Vec Nat (suc n) Have: Vec Nat (n +N 1) 如果我没有理解错的话，这些值不是... ...

在证明基本函数应用规律时，理解agda中的类型推理问题。

我正在尝试证明函数应用的身份法则。我对下面的所谓身份函数apfId，得到黄色高亮。我不明白，难道_≡_ {A}的类型不是 ...

将布尔语句提升为命题。

给定一个列表，一个 "属性"（一个函数到Bools），和一个证明any f xs≡真，我想得到一个Any（λ x → T（f x））ns的值，即我想让a把一个证明从any转换为Any的证明。到目前为止，我 ...

如何证明agda中简单语言的弱化？

我想证明一个类似于PFPL第4章中Harper的弱化定理，即弱化 : {x : String}。也就是说，弱化：{x : String}。{Γ : Context} {e : Expr} {τ τ': Type} → x ∉dom Γ → Γ ⊢ e ؛ τ' → (Γ , x ؛ τ) ⊢ e ؛......。

了解关于FSA和Agda中常规语言的简单证明的递归调用失败

我正在尝试证明，Agda中的简单FSA仅接受以0结尾的字符串-这是Sipser的书中的第一个示例。我不是将evalFSA用作谓词，而是将其作为函数，并且...

教类型检查器2 ^ e≢0

假设我对所有e：模块都显示2 ^ e≢0，在这里打开导入Data.Nat打开导入Data.Nat.DivMod打开导入Relation.Binary.PropositionalEquality假设2 ^e≢0：（e：ℕ ）...

消除类型级别的Maybe

是否有任何方法可以在类型级别解开Maybe monad内部的值？例如，如何为具有pred变体的Vecs定义类型安全的尾巴：pred：ℕ->也许ℕpred 0 ...