Repository Layout

The repository is organized as follows (listing the main folders and files):

• .github contains GitHub-specific configuration files and workflows.
  • workflows contains GitHub Actions workflow files.
    • lint.yml is the style lint workflow triggered on push and pull request events.
  • dependabot.yml is the configuration file to automate CI dependency updates.
• .vscode contains Visual Studio Code configuration files
  • extensions.json recommends VS Code extensions for the project.
  • settings.json defines the project-specific settings for VS Code.
• Project should contain the Lean code files.
  • Mathlib should contain .lean files with declarations missing from existing Mathlib developments.
  • ForMathlib should contain .lean files with new declarations to be upstreamed to Mathlib.
  • Example.lean is a sample Lean file.
• scripts contains scripts to update Mathlib ensuring that the latest version is fetched and integrated into the development environment.
• .gitignore specifies files and folders to be ignored by Git. and environment.
• CONTRIBUTING.md should provide the guidelines for contributing to the project.
• lakefile.toml is the configuration file for the Lake build system used in Lean projects.
• lean-toolchain specifies the Lean version and toolchain used for the project.