the binary expansion of 7 has three elements (you will find them at indexes Fin ... | Hacker News

Hacker Newsnew | past | comments | ask | show | jobs | submit

		cmrx64 24 days ago \| parent \| context \| favorite \| on: Some Junk Theorems in Lean 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.

alimw 23 days ago [–]

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.

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