Hacker News new | ask | show | jobs
by BalinKing 164 days ago
See my other comment—LangRust.lean is the same way.

EDIT: Just skimmed Completeness.lean, and it looks similar—at a glance, even the 3+-line proofs are very short and look a lot like boilerplate.
1 comments
trissim 164 days ago
Interesting that you're using em dashes in your comments. Those require Alt+0151 or copy-paste. Glass houses.
link
dwb 164 days ago
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.
link
BalinKing 164 days ago
Yeah, I'm on macOS (although even back on Windows, I used to use the Character Map all the time).
link
trissim 164 days ago
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."

link