Open nomeata opened 5 months ago
Floris suggests in https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Loogle.20is.20live!/near/434717352:
I love the "did you maybe mean" field in loogle. Ideally it should find more miscapitalized words: MeasureTheory.measure should suggest MeasureTheory.Measure and galoisconnection should suggest GaloisConnection.
MeasureTheory.measure
MeasureTheory.Measure
galoisconnection
GaloisConnection
Floris suggests in https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Loogle.20is.20live!/near/434717352:
I love the "did you maybe mean" field in loogle. Ideally it should find more miscapitalized words:
MeasureTheory.measureshould suggestMeasureTheory.Measureandgaloisconnectionshould suggestGaloisConnection.