an approach i'm finding increasingly productive is to break up a proof into parts i "obviously" believe to be true and shim them with `sorry`s, focusing on the rest of the argument. i'd previously always write top-down but now i just leave those unsolved and come back when the big picture is clear
the end is in sight! only one screen's worth of exercises left in the 3.6 section. been working on this one for three weeks 🤪
[github.com/gaearon/anal...](
noticed a (recent?) regression on the web — can anyone reproduce? can't select upwards more than one line with keyboard
[Selection regression on the we...](
the funny thing is that evan’s comment is obviously wrong (as in, in a technical sense). the protocols are not comparable in their scope (activitypub doesn’t try to solve scaling) but he insists on treating them as zero sum.
i think it’s why meta talks about AP. unlike atproto, it isn’t competition
RE:
)
for the first time, there will be a first-class way to tell React to deprioritize some part of the tree, an alternative to unmounting.
[Release Activity in Canary by ...](
one thing that blew my mind about working in Lean (and is still blowing my mind) is that “variables” (really, let bindings) and “function calls” are all infinitely unfoldable. i can just replace each variable with its definition, each function with its body, any no of levels deep, during a proof.
