AGDA 中案例拆分的未绑定变量

Question

我们一直在尝试一些 AGDA，基本上是在 AGDA 中播放 Lean 中的自然数部分。然而，对于不平等，我们遇到了一个错误，这个错误在这个问题的精益解决方案中是不存在的。

这是代码：

module minimalExample where

open import Agda.Builtin.Nat
open import Agda.Builtin.Equality
open import Agda.Builtin.Sigma

-- x ≤ x + 1
data _leq_ {x : Nat} {y : Nat} : Nat -> Nat -> Set where
    leqpr : (k : Nat) -> x + k ≡ y -> x leq y

leqSuccOfLeq : {x y : Nat} -> x leq y -> x leq (suc y)
leqSuccOfLeq ineq = leqpr {! ineq !} {!   !}

如果我们尝试对变量 ineq 进行大小写拆分，我们会收到以下错误：

Unbound variable i when checking that the expression ? has type Nat

我们假设我们的定义有问题，但我们不知道是什么。我们也已经尝试过使用 $\Sigma$ 的定义，但这并没有解决问题。此外，我们知道以归纳方式定义此定义更为常见，但在实际情况并非如此时将其作为练习。

有人知道如何解决这个问题吗？

编辑：gallais 强调的错误是根本错误，但是无界变量的错误仍然发生在自动案例拆分中。但是硬编码大小写拆分解决了这个问题。

Answer 1

data _leq_ {x : Nat} {y : Nat} : Nat -> Nat -> Set where
    leqpr : (k : Nat) -> x + k ≡ y -> x leq y

定义了一个带有 2 个隐式参数的族 (x & y) 和两个显式索引（分别设置为 x & y 在 leqpr 构造函数的 return 类型中）。

您可能打算写：

data _leq_ (x y : Nat) : Set where
    leqpr : (k : Nat) -> x + k ≡ y -> x leq y

AGDA 中案例拆分的未绑定变量

Unbound variable on case split in AGDA

agda