Zulip Chat Archive

Stream: general

Topic: timeout with nat division


view this post on Zulip Etienne Laurin (Dec 02 2019 at 23:44):

example : 4001 / 2 = 2000 := by refl

How can I prove that without (deterministic) timeout?

view this post on Zulip Mario Carneiro (Dec 02 2019 at 23:52):

by norm_num

view this post on Zulip Etienne Laurin (Dec 03 2019 at 00:02):

That works, thanks! Would it be worth adding to docs/tactics.md?

view this post on Zulip 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: May 16 2021 at 05:21 UTC