Zulip Chat Archive

Stream: new members

Topic: Lean Tutorial


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

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.

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.

Patrick Massot (May 22 2020 at 17:57):

James, you should try using le_add_of_nonneg_right

Kevin Buzzard (May 22 2020 at 18:02):

It was any%!


Last updated: Dec 20 2023 at 11:08 UTC