agda - 如何使用前提工作制作 Adga 函数

Question

我想对自然数进行减法运算。但是，该函数的参数有一个前提，即 forall a, b in N ；一个 >= 乙。所以我做了一些相关的功能:

data ℕ : Set where
    zero : ℕ
    suc : ℕ → ℕ

data _NotLessThan_ : (n m : ℕ) → Set where
    ZERO : zero NotLessThan zero
    SUC_ZERO : ∀ n → (suc n) NotLessThan zero
    STEP : ∀ m n → m NotLessThan n → (suc m) NotLessThan (suc n)

sub : (m n : ℕ) →  (a : m NotLessThan n) → ℕ
    sub zero (suc n) () -- zero - n can't return
    sub zero zero _ = zero
    sub (suc m) zero _ = (suc m)
    sub (suc x) (suc y) a = sub x y (x NotLessThan y)

但是，我得到了错误:

 Set !=< x NotLessThan y of type Set₁
 when checking that the expression x NotLessThan y has type
 x NotLessThan y

我发现类型是 x NotLessThan y，因为我异常(exception)。有没有类型错误？如何调试这种类型错误或如何声明一个函数来跳过类型检测错误？

Answer 1

表达式(x NotLessThan y) 不是(x NotLessThan y) 类型。 NotLessThan 是类型集(索引集)的数据定义。您可以使用定义的三个构造函数构造 NotLessThan 的元素。在这种情况下，您必须在 a 上进行模式修补，以获得适当的构造函数和您需要的类型的元素。所以最后一种情况是

sub (suc x) (suc y) (STEP _ _ a) = sub x y a