bool.tt

Stream: mathlib4

[Patrick Massot]

It seems that mathport is not translating tt to true and f to false or am I missing something?

[Kevin Buzzard]

Yeah this is another weird example where they're aligned but sometimes mathport doesn't play ball (this was all over the place in data.bool.basic or whatever it was, the first file I ever ported).

[Mario Carneiro]

did we track down why that is? do you have an example

[Kevin Buzzard]

I had assumed it was the same issue as "mathport sometimes doesn't align ne with Ne" which we were talking about in another thread.

[Mario Carneiro]

that was about dot notation

[Mario Carneiro]

people aren't usually using dot notation for tt

[Kevin Buzzard]

Mario Carneiro said:

did we track down why that is? do you have an example

https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/.23align/near/305399010

It got lost in my sea of questions about #align (it reminds me of 2017 when you were patiently answering my sea of questions about type theory)

[Kevin Buzzard]

Hmm, we can't see that example now because the porting program is just giving us a load of #print stuff for Data.Bool.Basic now.

[Gabriel Ebner]

We even have a mathport issue for it: https://github.com/leanprover-community/mathport/issues/167