You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Its not deprecated per leanprover/lean4#4106, but sure, we should include .toml for the templates.
Sent from [Proton Mail](https://proton.me/mail/home) for iOS
Le mer. 11 déc. 2024 à 01:41, Serhii Khoma < ***@***.***(mailto:Le mer. 11 déc. 2024 à 01:41, Serhii Khoma <<a href=)> a écrit :
lean files are deprecated as per https://github.com/leanprover-community/mathlib4/wiki/Using-mathlib4-as-a-dependency
but are used in https://github.com/lenianiva/lean4-nix/blob/main/templates/dependency/lakefile.lean
The text was updated successfully, but these errors were encountered: