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.
Kevin Buzzard (May 22 2020 at 17:26):
linarith will solve it, but if you want to find out the name of the function which will do it directly you can try
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
Kevin Buzzard (May 22 2020 at 18:02):
It was any%!
Last updated: May 16 2021 at 05:21 UTC