proof2' doesn't pass type checking

[grouzen]

Hi, I've been starting to read the book, and I can't get a code working:

proof₂′ : (A : Set) → A → A
proof₂′ _ x = x

proof₂ : (succ (succ zero)) even  → (succ (succ zero)) even
proof₂ x = proof₂′ ℕ x

The error that I've got:

(succ (succ zero) even) !=< ℕ of type Set when checking that the expression x has type ℕ

Probably I'm missing something, or there is a typo in the book

I have Agda 2.4.2.2

Thanks, Michael

[cjenkin2]

@grouzen

The error message you are getting is more helpful than you realize. Allow me to explain:

The type of x in proof₂ is "(succ (succ zero)) even". When you call proof₂′ however, you are telling it that the type is ℕ. These two types are not the same, so it gives you a type error.

This is definitely a typo on the part of the author.

[grouzen]

@cjenkin2 Yeah! I noticed this too (types are different at all), that's why I created this issue.