nursery

Stream: general

[Simon Hudon]

Nice README file in the nursery @Sean Leather ! What do you think about having a test directory mirroring the structure of the src directory so that we can find in test/foo.lean examples illustrating the use of src/foo.lean? I think we don't have to be strict on the creating of such file, but we should nudge people towards creating them so that you can explore the nursery through its test directory.

[Sean Leather]

Yep, that is a good idea.

[Sean Leather]

Alternatively, there could be an examples directory for what you describe and a test directory that is for tactics and things like in mathlib.