Comment on Some Junk Theorems in LeanparentComments−cmrx648mothe 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.−alimw8moThe 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.
Comments
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.