search

leanprover-community / lean4game

Server to host lean games.
https://adam.math.hhu.de
GNU General Public License v3.0
198 stars 35 forks source link

Filter identical hints #142

Closed joneugster closed 11 months ago

joneugster commented 1 year ago

Don't display consequtive identical hints

djvelleman commented 1 year ago

There can be cases in which identical hints are not consecutive. So perhaps a better description would be: don't display the same hint more than once.

joneugster commented 11 months ago

I fixed this now the way I intended it to work, i.e. preventing consecutive identical hints from showing up again. However, I'll raise your question about whether that's the right behaviour in #165 with Marcus.