Zulip Chat Archive

Stream: new members

Topic: creating a library of lemmas


rzeta0 (Oct 07 2024 at 00:48):

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 (Oct 07 2024 at 03:15):

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 (Oct 07 2024 at 05:36):

See previous discussion:
#general > Mathlib++


Last updated: May 02 2025 at 03:31 UTC