using exact

Stream: new members

[Robert Watson]

In the following I can not use exact x:

lemma even_add_one' {n : ℕ} : even (n + 1) → odd (n + 2) :=
begin
  intro h,
  have x : odd (n + 2) := even_add_one h,
 -- exact x
end

What's the issue here?

[Alex J. Best]

What issue do you see in the infoview? If I have

import data.nat.parity
lemma even_add_one' {n : ℕ} : even (n + 1) → odd (n + 2) :=
begin
  intro h,
  have x : odd (n + 2) := even_add_one h,
 -- exact x
end

I see

unknown identifier 'even_add_one'

on the line above exact, which is Lean saying the lemma you want doesn't exist

[Alex J. Best]

Is there another lemma in the code you have on your computer?

[Alex J. Best]

What version of mathlib are you using, perhaps something changed recently?

[Robert Watson]

lemma even_add_one {n : ℕ} : even n → odd (n + 1) :=
begin
  intro h,
  cases h with d hd,
  rw hd,
  use d,
end

This is from Example_Lean_Projects even_and_odd.lean.

[Alex J. Best]

With that code included everything works fine for me.

[Robert Watson]

It works only if I use: use x instead of exact x

[Alex J. Best]

What is the error message you see?

[Robert Watson]

Sorry...I've understood it now. There was code afterwards which was confusing me. I simply misread the info_view!! My bad!

[Robert Watson]

Is there a way to simplify the info_view to only show errors up to a certain point in the code?

[Robert Watson]

Or do I have to comment everything else out?

[Alex J. Best]

Are you using vscode? At least for me any lines with errors have some sort of red underline, and then putting the cursor on that line makes the top of the info-view display the error (under Messages below the Tactic state, you can close the All messages part of the window below with the little triangle).
The problems panel shows everything, but that normally isn't as good as the infoview