Zulip Chat Archive

Stream: general

Topic: contrapose and push_neg


view this post on Zulip 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!

view this post on Zulip 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).

view this post on Zulip 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: May 09 2021 at 19:11 UTC