Zulip Chat Archive

Stream: general

Topic: Heisenbug


view this post on Zulip Scott Morrison (Aug 26 2018 at 14:05):

I just found a Heisenbug: a proof that doesn't typecheck correctly, but if you add tactic.result >>= tactic.trace at the end, it does!

view this post on Zulip Simon Hudon (Aug 26 2018 at 14:43):

those are fun

view this post on Zulip Simon Hudon (Aug 26 2018 at 14:44):

I suspect that pretty printing either does some type checking (forcing some unification) or resolves some meta variables. You can try and see what is the smallest some term of the proof that you can print and which will fix the proof

view this post on Zulip Scott Morrison (Aug 26 2018 at 14:46):

I'm in the midst of further changes that will affect how my metavariables get handled, so I think I'm going to defer diagnosing this bug, hoping that if I don't look at it it will disappear permanently. :-)


Last updated: May 16 2021 at 05:21 UTC