This is a solid intro.
I had no idea Lean was so Haskell-y and readable/practical in this way! For some reason I assumed it was just a clunky abstruse prover IDE type of thing, I guess I conflated it with older coq/Rocq and all the gigantic illegible ai math papers in recent news
1 comment
[ 3.1 ms ] story [ 7.9 ms ] thread