leanprover-community/NNG4

Documentation for tactics and definitions missing

Closed this issue · 2 comments

b-reinke commented

At least in the version that is currently live on https://adam.math.hhu.de/#/g/hhu-adam/NNG4/, the documentation for the tactics and definitions in the "inventory" on the right side is missing. There are also some lemmas that have missing documentation.

joneugster commented

Thanks! There is right now a student working on refactoring the NNG (as a summer project), adding new levels etc. and once they're done we'll make sure all the documentation in the "inventory" is also on par.

joneugster commented

Cleanup, this has been addressed a long time ago