mirror of
https://github.com/SinTan1729/lean-talk-sp24.git
synced 2024-12-24 21:08:36 -06:00
chg: Renamed the project
This commit is contained in:
parent
89997aeb57
commit
531dd25bd1
4 changed files with 5 additions and 5 deletions
|
@ -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
|
3
LeanTalkSP24.lean
Normal file
3
LeanTalkSP24.lean
Normal file
|
@ -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
|
|
@ -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
|
||||
|
|
Loading…
Reference in a new issue