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