Zulip Chat Archive
Stream: lean4
Topic: intros; contradiction
Mac (Jul 01 2022 at 07:33):
Is there single tactic that does intros; contradiction or is that as terse as it gets? I am kind of surprised that contradiction doesn't already do this as part of its checking.
Last updated: May 02 2025 at 03:31 UTC