Zulip Chat Archive

Stream: general

Topic: Heisenbug

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!

Simon Hudon (Aug 26 2018 at 14:43):

those are fun

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

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: Aug 03 2023 at 10:10 UTC