import Lake
open Lake DSL

package «miniF2F-lean4» {
  moreLinkArgs := #[
    "-L./.lake/packages/LeanCopilot/.lake/build/lib",
    "-lctranslate2"
  ]
}




@[default_target]
lean_exe repl where
  root := `REPL.Main
  supportInterpreter := true



@[default_target]
lean_lib «MiniF2F» {
  -- add library configuration options here
}

require mathlib from git "https://github.com/leanprover-community/mathlib4"@"3cecb823a74ed737c6ebc115e515eba649ec7715"