Zulip Chat Archive
Stream: general
Topic: cc is unexpectedly fast
Kenny Lau (Aug 17 2018 at 06:02):
Kenny Lau (Aug 17 2018 at 06:03):
oh... it's cheating :P
Kenny Lau (Aug 17 2018 at 06:03):
theorem test : 1001 = 2000 → false := λ (H : 1001 = 2000), false.elim (false_of_true_eq_false (absurd H (nat.bit1_ne_bit0 500 1000)))
Johan Commelin (Aug 17 2018 at 06:12):
That's not cheating. That's being smart (-;
Last updated: May 02 2025 at 03:31 UTC