Zulip Chat Archive

Stream: general

Topic: contrapose and push_neg

Johan Commelin (Aug 01 2019 at 19:09):

@Patrick Massot Thanks a lot for these tactics! They are really nice, and they allow one to reason like a real grown-up mathematician!

Patrick Massot (Aug 01 2019 at 21:14):

You're welcome! It's purely a product of my undergraduate teaching with Lean. Those tactics are indeed unavoidable if you want Lean proofs to look like real proofs (unfortunately they are far from sufficient).

Johan Commelin (Aug 02 2019 at 07:50):

Should exfalso take an optional argument?
I can imagine exfalso foo working like exfalso; refine foo.

Last updated: Aug 03 2023 at 10:10 UTC