我试图证明以下说法 vecNat : ∀ {n} (xs : Vec ℕ n) → last (xs ∷ʳ 1) ≡ 1 但我对这个案子感到困惑。(x ∷ xs) vecNat5 : ∀ {n...

我有这个功能： natListLast : List ℕ → ℕ natListLast [] = 0 natListLast nats@(x ∷ xs) = v.last (v.fromList ...

我安装了 Agda 并开始玩。我试图定义一个相等类型，并提出了以下解决方案： data _≡_ {A : Set} : A -> A -> Set where refl : {x : A} -> ...

我正在尝试通过感应原理实现西格玛消除，但我不明白为什么很好，但在下面用约束误差突出显示黄色，因为这些程序是等效的。pr₁ 和 pr₁' 并非如此。pr₂pr₂' 请您解释一下错误，以及为什么 agd...

我正在尝试在 agda 中编写一个反向向量函数，但遇到了以下绊脚石 Goal: Vec Nat (suc n) Have: Vec Nat (n +N 1) 如果我理解正确的话，这些值并不是绝对...

在我的 Agda 程序中，我有一个小函数来检查字符串是否相等（例如简化）： open import Data.String.Base using (String) open import Date....

我目前正在阅读 Ulf Norell 的博士论文，他在论文中描述了 Agda 的实现。 在第 2.2 章（第 41 页）中，他关注的是与依赖类型的模式匹配，他指出，有些模式——即使它们是不相交的和详...