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: Dec 20 2023 at 11:08 UTC