Mathlib (data/nat/basic):
@[simp] lemma bodd_bit1 (n) : bodd (bit1 n) = tt := bodd_bit tt n
Synport:
@[simp]
theorem bodd_bit1 (n) : bodd (bit1 n) = tt :=
bodd_bit true n
This instance shows both tt being translated to true, as well as tt not being translated.
Mathlib (data/nat/basic):
Synport:
This instance shows both
ttbeing translated totrue, as well asttnot being translated.