Zulip Chat Archive

Stream: new members

Topic: Tutorials Possible Example Error


Michael (Aug 09 2021 at 18:33):

Hello, I am currently working through the tutorials and I think I have found a slight error in 03_forall_or.lean. The second example reads

example (f g :   ) : even_fun f  even_fun g   even_fun (f + g) :=
begin
  intros hf hg x,
  calc (f + g) (-x) = f (-x) + g (-x) : rfl
  ... = f x + g x : by rw [hf, hg]
end

but the goal is not resolved at the end. Should it instead be as follows?

example (f g :   ) : even_fun f  even_fun g   even_fun (f + g) :=
begin
  intros hf hg x,
  calc (f + g) (-x) = f (-x) + g (-x) : rfl
  ... = f x + g x : by rw [hf, hg]
  ... = (f + g) x : rfl
end

Adding that final line makes it say "goals accomplished".

Eric Rodriguez (Aug 09 2021 at 18:46):

does lean error without that line? i'd be kind of surprised if it was

Michael (Aug 09 2021 at 18:58):

Eric Rodriguez said:

does lean error without that line? i'd be kind of surprised if it was

I don't get a red underline error, it's just that the goal won't close. I'm guessing if I'm not getting a red underline error, then it's actually fine without?

Bryan Gin-ge Chen (Aug 09 2021 at 19:07):

That's right. If you want to see the goal closed at the end of a tactic block you can add a comma after the last line before end.


Last updated: Dec 20 2023 at 11:08 UTC