Wat is wrong with this definition?

Stream: new members

[Ken Roe]

inductive evv : ℕ -> Prop
| Base := (evv 0)
| Inductive := ∀ x, even x → even (x+2).

gives the following error:

invalid return type for 'evv.Base'

[Simon Hudon]

Try:

inductive evv : ℕ -> Prop
| Base : (evv 0)
| Inductive : ∀ x, evv x → evv (x+2).