search

leanprover-community / lean4game

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

local notation in inventory #216

Closed joneugster closed 3 months ago

joneugster commented 5 months ago

local notation like Finset.sum does not work in the inventory.

joneugster commented 3 months ago

Turns out this is something that cannot be fixed on the server, but has to be set in the game. Updated documentation.