Hacker Newsnew | past | comments | ask | show | jobs | submit | cmrx64's commentslogin

Contrariwise, I was part of the troupe of people that daily picked up these bags along walking trails. One of the few benefits of living in the USA: covert prosocial behavior is extremely common.

smell isn’t integrated in the thalamus with other sensory streams, it does something else entirely

A decade ago I ran several “seven hour roguelikes”, https://web.archive.org/web/20160321153532/http://people.cla... is the documentation from the first one.

The first year I spent six hours writing one of the first ecs crates in Rust and then an hour turning it into a game. lots of fun! you can search “7HRL” on github to find the historical participants not too ashamed to publicize their code at the end. A few dozen people enjoyed this.


List.TFAE is a helper definition and it’s invoked on a funny looking term when translated directly into english. I don’t know what I think, yeah it’s kinda junky but not in the way that 57 \mem 100 in a set encoding of the naturals.

    theorem TFAE_7_binary : List.TFAE (7).bits := by
  unfold Nat.bits Nat.binaryRec Nat.binaryRec; simp!


the binary expansion of 7 has three elements (you will find them at indexes Fin 0, Fin 1, and Fin 2) and the proof is of their equality.


The proof is actually of their equivalence as propositions. This is only possible because the binary digits are represented as Bools, and a Bool b can be coerced to the proposition that b = true.


the last paragraphs cite why junk theorems are objectionable but then fully misinterprets it to draw the opposite conclusion. the intersection is the S-feature and problematic. 1 + 2 = 4 is a “theorem beyond T” expressed in T theory.

don’t be mislead about what a junk theorem is!


Thank you. I was following along until that paragraph and got the opposite interpretation too.


Yah, I read that and thought "this seems like gibberish: maybe I am reading LLM slop".


rtld does a lot of work even in “static” binaries to rewrite relocations even in “unused parts” of any PIE (which should be all of them today) and most binaries need full dyld anyway.


That would deliver a blow to the integrity of the rest of that section because those sorts of upper bound constraints immediately reducible to “true” cannot cause backtracking of any kind.


https://ember.dev ’s deeper pages (not the blog, but the “resumelike” project pages) was written by claude with guidance and a substantial corpus of my own writing and i still couldn’t squash out all the GPTisms in the generation passes. probably net waste of time, for me, for writing.


whois (delegation files) according to the embedded blog post, eg https://ftp.arin.net/pub/stats/arin/delegated-arin-extended-...


Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: