proof - 类型的定义在 agda 中不起作用

Question

这个模算术的定义不能在 agda 中编译：

data mod (n : nat): n → Set where
    zeroM : mod n
    S : mod n → mod n
    equMod : { x : nat} → (x ≡ n) → (x ≡ zeroM)

错误：nat should be a sort, but isn’t

有人能帮我吗 ？

标签： proofagdadependent-type

Answer 1

当你写 n -> Set 你需要 n 是一个类型，但它是一个自然数。我猜你只是想写data mod (n : nat) : Set这意味着mod : nat -> Set。