Zulip Chat Archive

Stream: new members

Topic: Lean Tutorial


view this post on Zulip James Arthur (May 22 2020 at 17:22):

I am slightly confused on the Lean tutorial. I am at the following

import data.real.basic

example (a b : ) (ha : 0  a) (hb : 0  b) : 0  a + b :=
begin
  sorry
end

and can't seem to get anywhere.

Thanks, James

view this post on Zulip Kevin Buzzard (May 22 2020 at 17:26):

The tactic linarith will solve it, but if you want to find out the name of the function which will do it directly you can try library_search.

view this post on Zulip Patrick Massot (May 22 2020 at 17:56):

Kevin, this is fine when you're cheating in a speed-run against undergrads, but we're trying to teach something here.

view this post on Zulip Patrick Massot (May 22 2020 at 17:57):

James, you should try using le_add_of_nonneg_right

view this post on Zulip Kevin Buzzard (May 22 2020 at 18:02):

It was any%!


Last updated: May 16 2021 at 05:21 UTC