CODEWITHSUNDEEP
dependent-typeidris
Yang Bo
Yang Bo

Reputation: 3718

Why doesn't equality involving “minus” typecheck in Idris?

Why won't the following typecheck:

minusReduces : (n : Nat) -> n `minus` Z = n
minusReduces n = Refl

Yet this will typecheck fine:

plusReduces : (n : Nat) -> Z `plus` n = n
plusReduces n = Refl

Upvotes: 4

Views: 79

Answers (1)

Cactus
Cactus

Reputation: 27626

minus n doesn't reduce because minus is defined with pattern matching on the first argument:

total minus : Nat -> Nat -> Nat
minus Z        right     = Z
minus left     Z         = left
minus (S left) (S right) = minus left right

So you'll need to split your Z and S n cases as well:

minusReduces : (n : Nat) -> n `minus` Z = n
minusReduces Z = Refl
minusReduces (S k) = Refl

Upvotes: 6

Related Questions