Unhelpful hover text - Githubissues

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

Unhelpful hover text #174

Open joneugster opened 11 months ago

joneugster commented 11 months ago

if I hover over + I get

@HAdd.hAdd ℕ ℕ ℕ instHAdd a b : ℕ

a + b computes the sum of a and b. The meaning of this notation is type-dependent.

I think this is super-unhelpful. Is there anything we can do about this?

joneugster commented 11 months ago

Currently, hover texts and error messages are purely taken from lean, but some of them are really unhelpful. Fix this in lean or overwrite them in the game?