79773923

Date: 2025-09-24 15:44:56
Score: 1
Natty:
Report link

Okay, I mistakenly copied idris1's example code. Parity's definition should be:

data Parity : Nat -> Type where
     Even : {n : _} -> Parity (n + n)
     Odd  : {n : _} -> Parity (S (n + n))

In Idris 2, we need to state explicitly that n is needed at run time

When I leave that parameter out, Idris inserts {0 n : _} for me, which is has quantity 0.

In this case, the erased value j is being passed as the first argument to helpEven, which is not quantity 0.

However,

(Incidentally, also note that in Idris 2, names bound in types are also available in the definition without explicitly rebinding them.)

So helpEven doesn't need (j : Nat) at all. This could work too.

 helpEven : Parity (S j + S j) -> Parity (S (S (plus j j)))
 helpEven p = rewrite plusSuccRightSucc j j in p

...
parity (S (S (j + j))) | Even = helpEven (Even {n = S j})
...
Reasons:
  • Probably link only (1):
  • Long answer (-0.5):
  • Has code block (-0.5):
  • Self-answer (0.5):
  • Low reputation (0.5):
Posted by: Johnny Liao