News for hackers. Stuff that matters.

A comment on Show HN: Lean4 proof that SSOT requires definition-time hooks and introspection. Parent comment

Re:Show HN: Lean4 proof that SSOT requires definition-time h... by trissim on Thursday January 08, 2026 @02:39AM (#46538375)
Interesting that you're using em dashes in your comments. Those require Alt+0151 or copy-paste. Glass houses.
[ Parent | on HN ]
Re:Show HN: Lean4 proof that SSOT requires definition-time h... by dwb on Thursday January 08, 2026 @03:14AM (#46538601)
And Option-Shift-Hyphen in macOS, which is easy if you know it. And a press and hold on a hyphen on iOS, which is discoverable, even.
[ Parent | on HN ]
Re:Show HN: Lean4 proof that SSOT requires definition-time h... by BalinKing on Thursday January 08, 2026 @12:32PM (#46543823)
Yeah, I'm on macOS (although even back on Windows, I used to use the Character Map all the time).
[ Parent | on HN ]
Re:Show HN: Lean4 proof that SSOT requires definition-time h... by trissim on Thursday January 08, 2026 @01:16PM (#46544426)
Fair, the em dash comment was a cheap shot. Withdrawn.

The substantive point stands: you've now "skimmed" multiple files, called them all "boilerplate," and haven't engaged with the actual proof structure. The rebuttals section addresses "The Proofs Are Trivial" directly (Concern 9).

At some point "I skimmed it and it looks trivial" stops being a critique and starts being "I didn't read it."

[ Parent | on HN ]