English: huggermugger. It's so confusing (hugger + mugger = clandestine work) that you cannot just pass by it without rising an eyebrow.

Polish: dykteryjka (short, funny story) and imponderabilia (things which are incalculable, but affect other things, like luck, state of mind, or similar).

Tip for future QM problems: write n subscripts in phi and normalization factor. It's sometimes easy to lose the explicit relationship, and it's one of those omissions that can waste a lot of your time when it's least convenient.

What's your process of learning Coq? I have to confess that 'proof automation' is one of those shortcomings I never overcame. Even going through your well-documented code took me a shameful amount of time, and that's after you've done all the heavy lifting.

Agreed on Idris, but, per your recommendation back from IRC dwelling days, I found Type-Driven Development with Idris by E. Brady as much more accessible. In this case, it means "I went farther into it than into any Coq tutorial". :P

Hi there. It's Devac, have some account recovery problems and made an alt. Sorry if I didn't respond.

The last two weeks were a tad hectic. I met lots of people, continue playing and anxiously await news on the PhD placement front.

My cardiologist is retiring, but she recommended me to one of her past residents, and he's been both understanding and accommodating.

mk - I used a non-gmail email for this account and messages from Hubski aren't filtered out. It's Wirtualna Polska (wp.pl - can't link), which probably won't help anyone, but it might be relevant for your diagnostics.

Thanks, I'll give it a look sometime. Not much of a fan of 'prequels', but this looks both interesting and promising.

Also, sorry for using an alt.