feat: use module system -> add module keyword to the top - #13

Open

srghma wants to merge 1 commit into

digama0:masterfrom

srghma:use-module

srghma commented May 22, 2026

I have tried to use module system (using https://github.com/srghma/.dotfiles/blob/main/bin/lean_use_modules) but open private from Batteries stops working in this mode

Not sure what to do


          feat: use module system -> add module keyword to the top

f573aeb

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet