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):
exfalso take an optional argument?
I can imagine
exfalso foo working like
exfalso; refine foo.
Last updated: May 09 2021 at 19:11 UTC