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 referencelean_lib MyLibrary
to include a MyLibrary - we then create a
MyLibrary.lean
file whichimport
s the desired definitions, egimport MyLibrary.Naturals
- following the example,
MyLibrary
needs to be a folder, and inside that there needs to be aNaturals.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