Zulip Chat Archive
Stream: general
Topic: timeout with nat division
Etienne Laurin (Dec 02 2019 at 23:44):
example : 4001 / 2 = 2000 := by refl
How can I prove that without (deterministic) timeout?
Mario Carneiro (Dec 02 2019 at 23:52):
by norm_num
Etienne Laurin (Dec 03 2019 at 00:02):
That works, thanks! Would it be worth adding to docs/tactics.md?
Bryan Gin-ge Chen (Dec 03 2019 at 00:03):
Yes! There's actually a longstanding issue to improve the tactic docs here where that's mentioned.
Last updated: Dec 20 2023 at 11:08 UTC