import Lake
open Lake DSL

package repro
@[default_target] lean_lib Repro