fLT

Stream: general

[Kevin Buzzard]

Sometimes auto-generated instance names have got fLT in them. The first time I noticed this was in the FLT project which confused me for a while, but then I realised that it seemed to be a core Lean thing. Searching is difficult because I say FLT a lot more often than everyone else says fLT. What does it stand for/mean?

[Kenny Lau]

the theorem that says Foo Bar = 67 is supposed to be named foo_bar_eq_67, i.e. each word should start with a lowercase letter

[Thomas Zhu]

The code for that should be here: https://github.com/leanprover/lean4/blob/744f98064b056ee27fc8c97f524797c8cc96f436/src/Lean/Elab/DeclNameGen.lean#L199-L206. The docstring of the next function mkBaseNameWithSuffix says:

... it adds suffixes using the current module if the resulting name doesn't refer to anything defined in this module.

[Kevin Buzzard]

Oh OK so it really is an FLT thing! Thanks!

[Weiyi Wang]

Searching is difficult

My take on this is that searching should be case-insensitive

[Kenny Lau]

loogle searching by string is case-insensitive