creating a library of lemmas

Stream: new members

[rzeta0]

Following on from the previous discussion about whether mathlib would ever have a Nat.le_or_succ_le tactic, where the general consensus was "no", I am exploring how difficult it might be to have a library of useful beginner-friendly lemmas to go with the educational examples I am creating.

Documentation seems difficult to follow, so I wanted to check if the following is broadly correct:

• we start with lakefile.lean and include a reference lean_lib MyLibrary to include a MyLibrary
• we then create a MyLibrary.lean file which imports the desired definitions, eg import MyLibrary.Naturals
• following the example, MyLibrary needs to be a folder, and inside that there needs to be a Naturals.lean file with the actual lemma's defined (and proven).

I guessed the above by looking at Heather MacBeth's project files.

Is it possible to not have a folder and simple have a MyLibrary.lean file with the definitions? How would I reference this file (not folder) in lakefile.lean?

[Derek Rhodes]

Hi @rzeta0 , I used lake to initialize a project and removed the library directory and moved it's only contents, the default hello definition into the file meant for imports. It still builds fine. I don't think any other changes were necessary. Anyways, I pushed it out to github: https://github.com/drhodes/minilib

There are more docs about lake in the FPiL book in the Hello World > Getting Started section:

[Martin Dvořák]

See previous discussion:
#general > Mathlib++