lean#281 assumption?

Stream: PR reviews

[Jalex Stark]

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)

[Jalex Stark]

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