leanprover-community / mathlib

  • Home
  • Zulip archive
  • API documentation
  • Lean web editor
  • Links

Zulip Chat Archive

Stream: new members

Topic: Wat is wrong with this definition?


Ken Roe (Jul 24 2018 at 14:20):

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 (Jul 24 2018 at 14:24):

Try:

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

Last updated: May 02 2025 at 03:31 UTC

Theme Simple by wildflame © 2016 Powered by jekyll