A toy example of a Lean 4 project with two dependencies: a local dependency, which lives in the subdirectory localdep an external dependency, which lives at https://github.com/rwbarton/lean4-test/