4 ms·
This is a junk theorem, it's trying to prove something that will sound strange or meaningless but is technically allowed by the details of the foundations. Her
by tux3 10mo ago
This is a junk theorem, it's trying to prove something that will sound strange or meaningless but is technically allowed by the details of the foundations.
Here it's building a list with one element and saying all elements of this list are equivalent. S̶o̶ ̶t̶h̶e̶ ̶f̶o̶l̶l̶o̶w̶i̶n̶g̶ ̶e̶l̶e̶m̶e̶n̶t̶s̶ ̶o̶f̶ ̶t̶h̶e̶ ̶l̶i̶s̶t̶ ̶a̶r̶e̶ ̶a̶l̶l̶ ̶e̶q̶u̶i̶v̶a̶l̶e̶n̶t̶ ̶t̶o̶ ̶e̶a̶c̶h̶ ̶o̶t̶h̶e̶r̶ ̶(̶t̶h̶e̶r̶e̶ ̶i̶s̶ ̶a̶ ̶s̶i̶n̶g̶l̶e̶ ̶e̶l̶e̶m̶e̶n̶t̶ ̶i̶n̶ ̶t̶h̶e̶ ̶l̶i̶s̶t̶)̶
- cmrx64 10mo agothe 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 10mo agoThe 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.