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

forbidden keywords #215

Closed joneugster closed 3 weeks ago

joneugster commented 2 months ago 
./././Game.lean:94:0: warning: No world introducing else, but required by Trace
./././Game.lean:94:0: warning: No world introducing then, but required by Trace
./././Game.lean:94:0: warning: No world introducing clear, but required by Trace
./././Game.lean:94:0: warning: No world introducing if, but required by Trace
./././Game.lean:94:0: warning: No world introducing Fin, but required by Trace
joneugster commented 2 months ago

Only thing left: Why is Fin here?