search

leanprover-community / lean4game

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

Hint shows blue squiggle #211

Closed joneugster closed 1 month ago

joneugster commented 2 months ago

Seems that Hint now always shows the blue squiggle coming from the logInfo-hack to transport the hint into Statement

joneugster commented 1 month ago

I think that only happens in cases where there are some parsing errors