-rw-r--r-- 170 leangoppa-20230726/lakefile.lean rawimport Lake open Lake DSL package leangoppa require mathlib from git "https://github.com/leanprover-community/mathlib4.git" @[default_target] lean_lib Goppadecoding