followed tags: 0
followed domains: 0
badges given: 0 of 1
member for: 57 days
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).
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.