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