Zulip Chat Archive

Stream: PR reviews

Topic: lean#281 assumption?


view this post on Zulip Jalex Stark (Jun 04 2020 at 15:57):

in lean#281, @Gabriel Ebner and i tried to make an assumption?and a bunch of things broke because we changed the precedence of ?. (I'm trying to back out enough details to ask a question)

view this post on Zulip Jalex Stark (Jun 04 2020 at 16:07):

maybe the right answer is to do a binary search to find a precedence level that makes the tactic work but doesn't break a bunch of things


Last updated: May 06 2021 at 12:15 UTC