Live data from Hacker News

Viewing profile — hirple

hirple

HN member
Joined
Thu, Nov 26, 2020, 12:24 PM UTC
HN karma
32
Public activity
17 items

About hirple

CA. ML, formal verification.

email: hirple@corgi.coffee

Recent public activity

  1. comment
    Comment #38046763

    I've been interested in this question myself - and recently wrote a basic web 'microframework' for Lean 4 [1]. I've loved being able to use Lean's macro system to write JSX-like HT…

  2. comment
    Comment #34597468

    As a rule I find that people who take the common, simplistic, tweet-length view of British rule (i.e. that it became rich by stealing from India, that it was the deliberate invoker…

  3. comment
    Comment #33767016

    Somewhat related - does anyone use meow + paredit? I can’t find a clearly recommended way to combine the two as I can with boon.

  4. comment
    Comment #32654464

    For canal boating, absolutely. Maybe 20-30k for a cheaper boat. Can moor for free. Coal and fuel maybe £100 a month each, depending on how much you travel/if you have solar etc. Yo…

  5. comment
    Comment #31107063

    I assume you've taken a look at org-jira?

  6. comment
    Comment #28955509

    You should just be able to hit `$` in the magit buffer to watch the output.

  7. comment
    Comment #26978928

    I agree with you - but the standards elsewhere seem to be so much lower even than here that I think it's (possibly) worthwhile having political discussions on HN. Of course, I woul…

  8. comment
    Comment #26972475

    Speaking as a consultant, these are terrible slides.

  9. comment
    Comment #26347182

    I guess Coq/Lean standard libraries fit this definition.

  10. comment
    Comment #26251811

    Not true, we certainly have those that start at 8. Consider a ~45m commute and time to get ready, and waking up at 6 something is not unheard of. (I personally had to wake up at 5:…

  11. comment
    Comment #26025696

    McKinsey are involved in almost every company in the Fortune 500, and have been for decades. Of course they're going to be around for almost any given corporate failure.

  12. comment
    Comment #25960635

    Really interested in the 'custom pandas typechecker'. Are there any more details anywhere, or has anyone else tried writing something similar?

  13. comment
    Comment #25789461

    Hence it is impossible for an object (with mass) to reach c. Only progressively closer - 0.99c, 0.999c, 0.9999c etc.

  14. comment
    Comment #25633359

    org-babel might work here. There are also repl keybindings in python mode in emacs.

  15. comment
    Comment #25471323

    Not exactly this, but I've had some success using logic programming (minikanren) to statically assert certain facts about dataframes in spark. E.g. "if Row_a is filtered to Row_b, …

  16. comment
    Comment #25223538

    I'd be happy to help here too, let me know. I can try to hack some elisp together tomorrow. Looks like rope would be a decent place to start.

  17. comment
    Comment #25219372

    Curious what you prefer about PyCharm over emacs + LSP. I'm a pretty poor PyCharm power-user, so wondering what I"m missing.