`tt` is sometimes not translated

leanprover-community / mathport

Mathport is a tool for porting Lean3 projects to Lean4

Apache License 2.0

41 stars 15 forks source link

`tt` is sometimes not translated #167

Open gebner opened 2 years ago

gebner commented 2 years ago

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.

gebner commented 2 years ago

This happens because only the second tt has a resolved constant in the AST. Not sure why there is a difference between theorem statement and proof here.