Zulip Chat Archive

Stream: new members

Topic: using exact


Robert Watson (Mar 29 2022 at 13:01):

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 (Mar 29 2022 at 13:05):

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 (Mar 29 2022 at 13:06):

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

Alex J. Best (Mar 29 2022 at 13:08):

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

Robert Watson (Mar 29 2022 at 13:10):

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 (Mar 29 2022 at 13:11):

With that code included everything works fine for me.

Robert Watson (Mar 29 2022 at 13:13):

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

Alex J. Best (Mar 29 2022 at 13:13):

What is the error message you see?

Robert Watson (Mar 29 2022 at 13:14):

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

Robert Watson (Mar 29 2022 at 13:15):

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

Robert Watson (Mar 29 2022 at 13:16):

Or do I have to comment everything else out?

Alex J. Best (Mar 29 2022 at 13:20):

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


Last updated: Dec 20 2023 at 11:08 UTC