Search code examples
proofagdadependent-type

definition of a type doesn’t work in agda

This definition of modular arithmetic doesn’t compile in agda :

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

Error: nat should be a sort, but isn’t

Can someone help me ?

Solution

  • When you write n -> Set you need n to be a type but it is a natural number. I guess you just want to write data mod (n : nat) : Set which means that mod : nat -> Set.