Zulip Chat Archive

Stream: general

Topic: Still newbie

Patrick Massot (May 09 2018 at 16:16):

Aaaarg. It's been almost six month now. And I still waste time because I think Lean will accept to prove non sense such as

lemma False (N : ℕ) : 1 + (1 + (N - 1) - 1) = N :=
sorry

Patrick Massot (May 09 2018 at 16:18):

Gabriel, maybe vscode-lean should have a newbie option which, among other things, would trigger a warning popup each time it detects use of ℕ substraction. :disappointed:

Last updated: Dec 20 2023 at 11:08 UTC