diff --git a/Lean Talk SP24.lean b/Lean Talk SP24.lean deleted file mode 100644 index 68ca9d4..0000000 --- a/Lean Talk SP24.lean +++ /dev/null @@ -1,3 +0,0 @@ --- This module serves as the root of the `«Lean Talk SP24»` library. --- Import modules here that should be built as part of the library. -import «Lean Talk SP24».basics diff --git a/LeanTalkSP24.lean b/LeanTalkSP24.lean new file mode 100644 index 0000000..baa4c31 --- /dev/null +++ b/LeanTalkSP24.lean @@ -0,0 +1,3 @@ +-- This module serves as the root of the `«LeanTalkSP24»` library. +-- Import modules here that should be built as part of the library. +import «LeanTalkSP24».basics diff --git a/Lean Talk SP24/basics.lean b/LeanTalkSP24/basics.lean similarity index 100% rename from Lean Talk SP24/basics.lean rename to LeanTalkSP24/basics.lean diff --git a/lakefile.lean b/lakefile.lean index 734c0f1..7276908 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -1,7 +1,7 @@ import Lake open Lake DSL -package «Lean Talk SP24» where +package «LeanTalkSP24» where -- Settings applied to both builds and interactive editing leanOptions := #[ ⟨`pp.unicode.fun, true⟩, -- pretty-prints `fun a ↦ b` @@ -13,5 +13,5 @@ require mathlib from git "https://github.com/leanprover-community/mathlib4.git" @[default_target] -lean_lib «Lean Talk SP24» where +lean_lib «LeanTalkSP24» where -- add any library configuration options here