### Add Lean Documentation Example Tests

Source: https://github.com/leanprover/lean4/blob/master/src/shell/CMakeLists.txt

Dynamically finds all `.lean` files in the `doc/examples` directory and adds a CMake test for each, excluding files starting with `.#`. Each test executes `test_single.sh` in the respective directory with the found Lean file as an argument.

```cmake
file(GLOB LEANDOCEXS "${LEAN_SOURCE_DIR}/../doc/examples/*.lean")
FOREACH(T ${LEANDOCEXS})
  if(NOT T MATCHES "\\.#")
    GET_FILENAME_COMPONENT(T_NAME ${T} NAME)
    add_test(NAME "leandocex_${T_NAME}"
             WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../doc/examples"
             COMMAND bash -c "${TEST_VARS} ./test_single.sh ${T_NAME}")
  endif()
ENDFOREACH(T)
```

--------------------------------

### Install Lean Extension in WSL via VS Code

Source: https://github.com/leanprover/lean4/blob/master/doc/make/wsl.md

Command to install the Lean 4 extension directly into your WSL environment from within Visual Studio Code. This ensures the extension runs within the Linux subsystem.

```shell
Install in WSL: Ubuntu
```

--------------------------------

### Add Lean Compiler Doc Example Test

Source: https://github.com/leanprover/lean4/blob/master/src/shell/CMakeLists.txt

Adds a CMake test for the documentation examples within the compiler tests. This test builds the example using `leanmake` and then runs a specific test case ('hello world').

```cmake
add_test(NAME leancomptest_doc_example
         WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../doc/examples/compiler"
         COMMAND bash -c "export ${TEST_VARS}; leanmake --always-make bin && ./build/bin/test hello world")
```

--------------------------------

### Install Standard Library (CMake)

Source: https://github.com/leanprover/lean4/blob/master/CMakeLists.txt

Defines an installation command using CMake's 'CODE' directive. It executes a process to run 'make install' within the 'stage1' directory.

```cmake
install(CODE "execute_process(COMMAND make -C stage1 install)")

```

--------------------------------

### Install Lean Project Files with CMake

Source: https://github.com/leanprover/lean4/blob/master/src/CMakeLists.txt

This CMake snippet handles the installation of project files, specifically targeting .lean and .md files, while excluding the 'examples' directory. It installs files from the source directory to the 'src/lean' destination.

```cmake
install(DIRECTORY "${CMAKE_SOURCE_DIR}/" DESTINATION src/lean
        FILES_MATCHING
        PATTERN "*.lean"
        PATTERN "*.md"
        PATTERN examples EXCLUDE)
```

--------------------------------

### Install Lean Project Files with CMake

Source: https://github.com/leanprover/lean4/blob/master/stage0/src/CMakeLists.txt

This CMake script handles the installation of Lean project files, including source files and documentation. It uses file matching patterns to include specific file types and exclude directories like 'examples'. It also conditionally installs license files based on the build stage and configuration.

```cmake
install(DIRECTORY "${CMAKE_SOURCE_DIR}/" DESTINATION src/lean
        FILES_MATCHING
        PATTERN "*.lean"
        PATTERN "*.md"
        PATTERN examples EXCLUDE)

if(${STAGE} GREATER 0 AND INSTALL_LICENSE)
  install(FILES "${CMAKE_SOURCE_DIR}/../LICENSE" "${CMAKE_SOURCE_DIR}/../LICENSES" DESTINATION ".")
endif()

file(COPY ${CMAKE_SOURCE_DIR}/include/lean DESTINATION ${CMAKE_BINARY_DIR}/include
  FILES_MATCHING PATTERN "*.h")
```

--------------------------------

### Verbose Make Output

Source: https://github.com/leanprover/lean4/blob/master/doc/make/index.md

Provides instructions on how to enable verbose output when running the 'make' command during the Lean 4 build process. This is useful for troubleshooting by showing the exact commands being executed.

```bash
make VERBOSE=1
```

--------------------------------

### Clone and Build Lean4 Project

Source: https://github.com/leanprover/lean4/blob/master/doc/make/index.md

This snippet demonstrates the basic steps to clone the Lean 4 repository from GitHub, navigate into the directory, and configure and build the project using CMake presets. It specifies a parallelized release build and how to adjust the parallelism level.

```bash
git clone https://github.com/leanprover/lean4
cd lean4
cmake --preset release
make -C build/release -j$(nproc || sysctl -n hw.logicalcpu)
```

--------------------------------

### Configure Lean Server Logging Path in VS Code

Source: https://github.com/leanprover/lean4/blob/master/doc/make/wsl.md

JSON configuration for Visual Studio Code to set the server logging path for Lean 4. Setting this to a relative path like 'logs' ensures logs are created within the WSL project directory, avoiding Windows path issues.

```json
{
  "lean4.serverLogging.path": "logs"
}
```

--------------------------------

### Lean 4 Library Module: `Hello/Basic.lean`

Source: https://github.com/leanprover/lean4/blob/master/src/lake/README.md

An example Lean 4 module file defining a simple string constant. This file is part of the library and can be imported by other modules or the main executable.

```lean
def hello := "world"
```

--------------------------------

### Target Specification Syntax Patterns

Source: https://github.com/leanprover/lean4/blob/master/stage0/src/lake/README.md

Reference guide showing standardized syntax patterns for specifying build targets in Lake CLI commands and configuration files. Supports package qualification, module prefixes, and facet selection.

```text
[@[<package>]/][<target>|[+]<module>][:<facet>]
```

--------------------------------

### Installation and Cleanup Targets

Source: https://github.com/leanprover/lean4/blob/master/stage0/src/CMakeLists.txt

Handles copying build artifacts to installation directories and defines cleanup targets. It copies `leanmake` to the bin directory, installs programs like `CADICAL` if conditions are met, and provides targets to clean intermediate files like `lib` and `.olean` files.

```cmake
file(COPY ${LEAN_SOURCE_DIR}/bin/leanmake DESTINATION ${CMAKE_BINARY_DIR}/bin)

install(DIRECTORY "${CMAKE_BINARY_DIR}/bin/" USE_SOURCE_PERMISSIONS DESTINATION bin)

if (${STAGE} GREATER 0 AND CADICAL AND INSTALL_CADICAL)
  install(PROGRAMS "${CADICAL}" DESTINATION bin)
endif()

add_custom_target(clean-stdlib
  COMMAND rm -rf "${CMAKE_BINARY_DIR}/lib" || true)

add_custom_target(clean-olean
  DEPENDS clean-stdlib)

install(DIRECTORY "${CMAKE_BINARY_DIR}/lib/" DESTINATION lib
  PATTERN temp EXCLUDE
  PATTERN "*.export" EXCLUDE
  PATTERN "*.hash" EXCLUDE
  PATTERN "*.trace" EXCLUDE
  PATTERN "*.rsp" EXCLUDE)

# symlink source into expected installation location for go-to-definition, if file system allows it
file(MAKE_DIRECTORY ${CMAKE_BINARY_DIR}/src)
# get rid of all files in `src/lean` that may have been loaded from the cache

```

--------------------------------

### Lean4 Theorem Naming Example: HashMap getElem?

Source: https://github.com/leanprover/lean4/blob/master/doc/std/naming.md

This Lean4 code snippet demonstrates a theorem about Std.HashMap.getElem?. It serves as an example for applying the naming algorithm, illustrating how the theorem's type and structure contribute to its generated name.

```Lean4
example {α : Type u} {β : Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α]
    [Inhabited β] {m : Std.HashMap α β} {a : α} {h' : a ∈ m} : m[a]? = some (m[a]'h') :=
  sorry
```

--------------------------------

### Install Binaries (CMake)

Source: https://github.com/leanprover/lean4/blob/master/src/CMakeLists.txt

Installs the contents of the binary directory's `bin` folder to the system's `bin` location, preserving source permissions.

```cmake
install(DIRECTORY "${CMAKE_BINARY_DIR}/bin/" USE_SOURCE_PERMISSIONS DESTINATION bin)
```

--------------------------------

### Install Library Files (CMake)

Source: https://github.com/leanprover/lean4/blob/master/src/CMakeLists.txt

Installs library files from `${CMAKE_BINARY_DIR}/lib/` to the system's `lib` directory. It excludes specific file patterns like `temp`, `.export`, `.hash`, `.trace`, and `.rsp` from the installation.

```cmake
install(DIRECTORY "${CMAKE_BINARY_DIR}/lib/" DESTINATION lib
  PATTERN temp EXCLUDE
  PATTERN "*.export" EXCLUDE
  PATTERN "*.hash" EXCLUDE
  PATTERN "*.trace" EXCLUDE
  PATTERN "*.rsp" EXCLUDE)
```

--------------------------------

### Configure Installation Prefix and Suffix with CMake

Source: https://github.com/leanprover/lean4/blob/master/stage0/src/CMakeLists.txt

This CMake script configures the installation prefix for the Lean project. It allows setting a custom installation prefix and appends system-specific suffixes (like the OS name) to it, ensuring proper installation paths across different environments. It uses cache variables for flexibility.

```cmake
set(LEAN_INSTALL_PREFIX "" CACHE STRING "If set, set CMAKE_INSTALL_PREFIX to this value + version name")
if(LEAN_INSTALL_PREFIX)
  string(TOLOWER ${CMAKE_SYSTEM_NAME} LOWER_SYSTEM_NAME)
  set(LEAN_INSTALL_SUFFIX "-${LOWER_SYSTEM_NAME}" CACHE STRING "If LEAN_INSTALL_PREFIX is set, append this value to CMAKE_INSTALL_PREFIX")
  set(CMAKE_INSTALL_PREFIX "${LEAN_INSTALL_PREFIX}/lean-${LEAN_VERSION_STRING}${LEAN_INSTALL_SUFFIX}")
endif()
```

--------------------------------

### Lean 4: Single-line Documentation Comment

Source: https://github.com/leanprover/lean4/blob/master/doc/std/style.md

Provides an example of a single-line documentation comment in Lean 4. The comment starts with `/--` and ends with `-/` on the same line, followed by the documented declaration. This format is used for concise explanations.

```lean
/- Carries out a monadic action on each mapping in the hash map in some order. -/
@[inline] def forM (f : (a : α) → β a → m PUnit) (b : Raw α β) : m PUnit :=
  b.buckets.forM (AssocList.forM f)

```

--------------------------------

### Run Lean 4 Executable

Source: https://github.com/leanprover/lean4/blob/master/src/lake/README.md

Executes a compiled Lean 4 program. The executable is typically found in the `.lake/build/bin` directory after running `lake build`. This example runs the `hello` executable.

```bash
.\/.lake/build/bin/hello
```

--------------------------------

### Interactive Server Test Example

Source: https://github.com/leanprover/lean4/blob/master/doc/dev/testing.md

Demonstrates how to write interactive tests for the Lean Language Server Protocol. Uses special comments to simulate client requests at specific code positions.

```lean
open Foo in
theorem tst2 (h : a ≤ b) : a + 2 ≤ b + 2 :=
Bla.
  --^ completion
```

--------------------------------

### Lean 4 Docstring Formatting for Theorems and Axioms

Source: https://github.com/leanprover/lean4/blob/master/doc/style.md

Demonstrates the correct formatting for docstrings accompanying theorems and axioms in Lean 4. It shows how to provide English explanations, including common names for axioms and their implications. Examples cover symmetric equality and propositional inequality.

```lean
/--
Equality is symmetric: if `a = b` then `b = a`.
-/
@[symm] theorem Eq.symm {α : Sort u} {a b : α} (h : Eq a b) : Eq b a :=
  h ▸ rfl

/--
Propositional inequality of natural numbers implies Boolean inequality.
-/
theorem Nat.ble_eq_true_of_le (h : LE.le n m) : Eq (Nat.ble n m) true :=
  match h with
  | Nat.le.refl   => Nat.ble_self_eq_true n
  | Nat.le.step h => Nat.ble_succ_eq_true (ble_eq_true_of_le h)
```

```lean
/--
Propositional Extensionality.

If two propositions are logically equivalent (that is, if each implies the other),
then they are equal; each may replace the other in all contexts.
-/
axiom propext {a b : Prop} : (a ↔ b) → a = b

/--
The Axiom of Choice.

`Nonempty α` is a proof that `α` has an element, but the element itself is
erased. The axiom `choice` supplies a particular element of `α` given only
this proof.

In particular, this axiom is
[global choice](https://en.wikipedia.org/wiki/Axiom_of_global_choice), which
is slightly stronger than the axiom of choice in ZFC.

The axiom of choice is used to derive the law of the excluded middle
(`Classical.em`), so it may show up in axiom listings for proofs that do
not obviously use choice.

This axiom can be used to construct “data” (that is, elements of non-Prop
types). There is no algorithmic interpretation of this axiom, so any definition
that would involve executing `Classical.choice` or other axioms must be marked
`noncomputable`. The compiler will not produce executable code for such
definitions, but they can be reasoned about in the logic.
-/
axiom Classical.choice {α : Sort u} : Nonempty α → α
```

--------------------------------

### Lean4 Theorem Naming Example: List IsPrefix Reverse

Source: https://github.com/leanprover/lean4/blob/master/doc/std/naming.md

This Lean4 code snippet presents a theorem about the interaction between List.IsPrefix and the reverse operation on lists. It serves as another example for the naming algorithm, highlighting how related concepts are named.

```Lean4
example : l₁ <+: l₂ → reverse l₁ <:+ reverse l₂ := sorry
```

--------------------------------

### Write and Execute Lake Script with Arguments

Source: https://github.com/leanprover/lean4/blob/master/stage0/src/lake/README.md

Define a script in lakefile.lean that accepts command-line arguments and can be executed via `lake script run`. The script demonstrates parameter handling and conditional logic using Lean's ScriptM monad. Dependencies include the Lake library and proper Lean installation.

```lean
import Lake
open Lake DSL

package scripts

/--
Display a greeting

USAGE:
  lake run greet [name]

Greet the entity with the given name. Otherwise, greet the whole world.
-/
script greet (args) do
  if h : 0 < args.length then
    IO.println s!"Hello, {args[0]'h}!"
  else
    IO.println "Hello, world!"
  return 0
```

--------------------------------

### CMake: Build Type and Testing Setup

Source: https://github.com/leanprover/lean4/blob/master/src/CMakeLists.txt

Ensures a build type is selected, defaulting to 'Release' if none is specified. It enables colorized output for Makefiles and initializes the testing framework.

```cmake
if (NOT CMAKE_BUILD_TYPE)
  message(STATUS "No build type selected, default to Release")
  set(CMAKE_BUILD_TYPE "Release")
endif()

set(CMAKE_COLOR_MAKEFILE ON)
enable_testing()
```

--------------------------------

### CMake C/C++ Compiler Configuration

Source: https://github.com/leanprover/lean4/blob/master/doc/make/index.md

Details how to specify custom C and C++ compilers for the Lean 4 build process using CMake. It notes that official Lean releases typically use Clang and references the CI configuration for more details.

```cmake
-DCMAKE_C_COMPILER=
-DCMAKE_CXX_COMPILER=
```

--------------------------------

### Lean 4 Library Root: `Hello.lean`

Source: https://github.com/leanprover/lean4/blob/master/src/lake/README.md

The root file for a Lean 4 library. It serves to import other modules within the library, making them accessible under the library's namespace. Imports the `Basic` module in this example.

```lean
-- This module serves as the root of the `Hello` library.
-- Import modules here that should be built as part of the library.
import «Hello».Basic
```

--------------------------------

### Install CCache Caching Compiler on OS X

Source: https://github.com/leanprover/lean4/blob/master/doc/make/osx-10.9.md

Installs CCache via Homebrew on macOS. This is a recommended optional package that caches C/C++ compilation results to significantly speed up rebuild times when building Lean4.

```bash
brew install ccache
```

--------------------------------

### Lean 4 `do` Notation: Early Return Example

Source: https://github.com/leanprover/lean4/blob/master/doc/std/style.md

Demonstrates the use of `do` notation in Lean 4 for conditional logic with an early return. It shows how to handle potential errors or missing values using a `let` match with a fallback condition.

```Lean
def getFunDecl (fvarId : FVarId) : CompilerM FunDecl := do
  let some decl ← findFunDecl? fvarId | throwError "unknown local function {fvarId.name}"
  return decl
```

--------------------------------

### Install Project Licenses with CMake

Source: https://github.com/leanprover/lean4/blob/master/src/CMakeLists.txt

Conditionally installs LICENSE and LICENSES files to the root of the installation directory. This action is performed only when the 'STAGE' variable is greater than 0 and the 'INSTALL_LICENSE' flag is true.

```cmake
if(${STAGE} GREATER 0 AND INSTALL_LICENSE)
  install(FILES "${CMAKE_SOURCE_DIR}/../LICENSE" "${CMAKE_SOURCE_DIR}/../LICENSES" DESTINATION ".")
endif()
```

--------------------------------

### Install Cadical (CMake)

Source: https://github.com/leanprover/lean4/blob/master/src/CMakeLists.txt

Conditionally installs the Cadical executable to the `bin` directory if the `CADICAL` variable is defined and `INSTALL_ প্রস্থ` is true, and the build stage is greater than 0.

```cmake
if (${STAGE} GREATER 0 AND CADICAL AND INSTALL_CADICAL)
  install(PROGRAMS "${CADICAL}" DESTINATION bin)
endif()

```

--------------------------------

### Execute Speedcenter Benchmark Suite with temci

Source: https://github.com/leanprover/lean4/blob/master/tests/bench/README.md

Executes the Speedcenter benchmark suite using the temci tool. It requires a local Lean build and temci to be installed. The command saves results to 'base.yaml' and can be customized with flags like '--runs' and '--included_blocks'.

```shell
temci exec --config speedcenter.yaml --out base.yaml
```

--------------------------------

### Build Lake from Source with Parallel Jobs

Source: https://github.com/leanprover/lean4/blob/master/stage0/src/lake/README.md

Execute the pre-packaged build.sh shell script to compile Lake from source, with optional parallelization using the -jX flag. This approach works without requiring an existing Lake installation. The resulting binary and library files are output to .lake/build directories.

```shell
./build.sh -j4
```

--------------------------------

### Install Required Build Packages via Homebrew on OS X

Source: https://github.com/leanprover/lean4/blob/master/doc/make/osx-10.9.md

Installs essential dependencies required to build Lean4 on macOS: CMake (build system), GMP (arbitrary precision arithmetic), libuv (asynchronous I/O), and pkgconf (package configuration utility).

```bash
brew install cmake
brew install gmp
brew install libuv
brew install pkgconf
```

--------------------------------

### Lean 4 `do` Notation: Multi-line `let` Match

Source: https://github.com/leanprover/lean4/blob/master/doc/std/style.md

Illustrates multi-line `let` matching within Lean 4's `do` notation. This example shows how to break down a complex `let` binding across multiple lines for improved readability, especially when the matched term is lengthy.

```Lean
def getFunDecl (fvarId : FVarId) : CompilerM FunDecl := do
  let some decl ←
        findFunDecl? fvarId
    | throwError "unknown local function {fvarId.name}"
  return decl
```

--------------------------------

### Install LLVM and LLD via Homebrew on OS X

Source: https://github.com/leanprover/lean4/blob/master/doc/make/osx-10.9.md

Installs LLVM toolchain and LLD linker via Homebrew on macOS. This provides an alternative clang++ compiler for building Lean4 as an option to Apple's pre-shipped version.

```bash
brew install llvm lld
```

--------------------------------

### Install GCC via Homebrew on OS X

Source: https://github.com/leanprover/lean4/blob/master/doc/make/osx-10.9.md

Installs the GNU Compiler Collection via Homebrew package manager on macOS. This provides an alternative C++14-compatible compiler for building Lean4 as an option to Apple's native clang++.

```bash
brew install gcc
```

--------------------------------

### CMake Build Type Configuration

Source: https://github.com/leanprover/lean4/blob/master/doc/make/index.md

Specifies how to configure the build type for the Lean 4 project using CMake. It lists the valid options for `-DCMAKE_BUILD_TYPE`, including RELEASE, DEBUG, RELWITHDEBINFO, and MINSIZEREL, with RELEASE being the default.

```cmake
-DCMAKE_BUILD_TYPE=RELEASE
```

--------------------------------

### Define and Run a Script in Lake

Source: https://github.com/leanprover/lean4/blob/master/src/lake/README.md

Demonstrates how to declare a custom script within a `lakefile.lean`. Scripts are defined as functions returning `ScriptM UInt32` and can be executed using `lake script run`. This example shows a simple script that takes an optional argument.

```lean
import Lake
open Lake DSL

package scripts

/--
Display a greeting

USAGE:
  lake run greet [name]

Greet the entity with the given name. Otherwise, greet the whole world.
-/    script greet (args) do
      if h : 0 < args.length then
        IO.println s!"Hello, {args[0]'h}!"
      else
        IO.println "Hello, world!"
      return 0
```

--------------------------------

### Lean4 Theorem Naming Example: HashMap contains

Source: https://github.com/leanprover/lean4/blob/master/doc/std/naming.md

This Lean4 code snippet demonstrates a theorem about Std.HashMap.contains and its relation to getElem?. It serves as an example for the naming algorithm, showing how a theorem derived from a condition (contains = false) is named.

```Lean4
theorem Std.HashMap.getElem?_eq_none_of_contains_eq_false {a : α} : m.contains a = false → m[a]? = none := sorry
```

--------------------------------

### Lean Structure Field Memory Order Example

Source: https://github.com/leanprover/lean4/blob/master/doc/dev/ffi.md

Illustrates the memory layout of a Lean structure `S` after reordering based on Lean's rules for C interop. This example shows the final memory order and the corresponding C accessors for each field.

```lean
structure S where
  ptr_1 : Array Nat
  usize_1 : USize
  sc64_1 : UInt64
  sc64_2 : { x : UInt64 // x > 0 } -- wrappers of scalars count as scalars
  sc64_3 : Float -- `Float` is 64 bit
  sc8_1 : Bool
  sc16_1 : UInt16
  sc8_2 : UInt8
  sc64_4 : UInt64
  usize_2 : USize
  sc32_1 : Char -- trivial wrapper around `UInt32`
  sc32_2 : UInt32
  sc16_2 : UInt16
```

--------------------------------

### Lean 4: Deriving Clause Example

Source: https://github.com/leanprover/lean4/blob/master/doc/std/style.md

Illustrates the correct usage and indentation of the `deriving` clause in Lean 4. The `deriving` clause should be unindented, similar to declaration bodies. This example shows how to derive the `Inhabited` instance for a `ByteArray` structure.

```lean
structure Iterator where
  array : ByteArray
  idx : Nat
deriving Inhabited
```

--------------------------------

### Lean4 Theorem Naming Example: List head? iff

Source: https://github.com/leanprover/lean4/blob/master/doc/std/naming.md

This Lean4 code snippet defines a biconditional theorem for List.head?. It serves as an example emphasizing the importance of including 'iff' in theorem names for clarity, especially when it distinguishes theorems that might otherwise have ambiguous names.

```Lean4
theorem List.head?_eq_none_iff : l.head? = none ↔ l = [] := sorry
```

--------------------------------

### Configure Lean Interactive Server Tests

Source: https://github.com/leanprover/lean4/blob/master/src/shell/CMakeLists.txt

This setup tests the interactive Lean server. It searches for `.lean` files in the `interactive` test directory, excluding temporary files and `run.lean`. Each valid file is added as a test, executing a bash script to verify interactive server behavior.

```cmake
file(GLOB LEANTESTS "${LEAN_SOURCE_DIR}/../tests/lean/interactive/*.lean")
FOREACH(T ${LEANTESTS})
  if(NOT T MATCHES "\\.#" AND NOT T MATCHES "run.lean")
    GET_FILENAME_COMPONENT(T_NAME ${T} NAME)
    add_test(NAME "leaninteractivetest_${T_NAME}"
             WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean/interactive"
             COMMAND bash -c "${TEST_VARS} ./test_single.sh ${T_NAME}")
  endif()
ENDFOREACH(T)
```

--------------------------------

### Whitespace Rules for Syntactic Elements in Lean 4

Source: https://github.com/leanprover/lean4/blob/master/doc/std/style.md

Demonstrates correct whitespace usage around syntactic elements like `:`, `:=`, `|`, `::`, `,`, and `;` in Lean 4. It also shows examples of correctly formatted function parameters and terms, including tuple and structure instances.

```Lean
def MacroScopesView.isPrefixOf (v₁ v₂ : MacroScopesView) : Bool :=
  v₁.name.isPrefixOf v₂.name &&
  v₂.scopes == v₂.scopes &&
  v₁.mainModule == v₂.mainModule &&
  v₁.imported == v₂.imported

example : Nat :=
  functionWithAVeryLongNameSoThatSomeArgumentsWillNotFit firstArgument secondArgument
    (firstArgumentWithAnEquallyLongNameAndThatFunctionDoesHaveMoreArguments firstArgument
      secondArgument)
    secondArgument

example : Nat × Nat :=
  ⟨imagineThisWasALongTerm,
   imagineThisWasAnotherLongTerm⟩

example : Vector Nat :=
  #v[imagineThisWasALongTerm,
     imagineThisWasAnotherLongTerm]

```

--------------------------------

### Add Lean Unit Tests

Source: https://github.com/leanprover/lean4/blob/master/src/shell/CMakeLists.txt

Dynamically finds all `.lean` files in the `tests/lean` directory and adds a CMake test for each, excluding files starting with `.#`. Each test executes `test_single.sh` in the respective directory with the found Lean file as an argument.

```cmake
file(GLOB LEANTESTS "${LEAN_SOURCE_DIR}/../tests/lean/*.lean")
FOREACH(T ${LEANTESTS})
  if(NOT T MATCHES "\\.#")
    GET_FILENAME_COMPONENT(T_NAME ${T} NAME)
    add_test(NAME "leantest_${T_NAME}"
             WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean"
             COMMAND bash -c "${TEST_VARS} ./test_single.sh ${T_NAME}")
  endif()
ENDFOREACH(T)
```

--------------------------------

### Lean4 Theorem Naming Examples: Nat Multiplication

Source: https://github.com/leanprover/lean4/blob/master/doc/std/naming.md

These Lean4 code snippets define theorems concerning multiplication by zero for natural numbers. They illustrate how the order of arguments can lead to distinct, yet related, theorem names and highlight the importance of clear naming.

```Lean4
theorem Nat.mul_zero (n : Nat) : n * 0 = 0 := sorry
theorem Nat.zero_mul (n : Nat) : 0 * n = 0 := sorry
```

--------------------------------

### Configure macOS Build Flags (CMake)

Source: https://github.com/leanprover/lean4/blob/master/src/CMakeLists.txt

Sets build flags for macOS, focusing on dynamic library loading and installation names. It configures install names for various shared libraries (`INIT`, `lean`, `Lake`) and sets runtime paths for executables.

```cmake
elseif(${CMAKE_SYSTEM_NAME} MATCHES "Darwin")
  string(APPEND CMAKE_CXX_FLAGS " -ftls-model=initial-exec")
  string(APPEND INIT_SHARED_LINKER_FLAGS " -install_name @rpath/libInit_shared.dylib")
  string(APPEND LEANSHARED_1_LINKER_FLAGS " -install_name @rpath/libleanshared_1.dylib")
  string(APPEND LEANSHARED_2_LINKER_FLAGS " -install_name @rpath/libleanshared_2.dylib")
  string(APPEND LEANSHARED_LINKER_FLAGS " -install_name @rpath/libleanshared.dylib")
  string(APPEND LAKESHARED_LINKER_FLAGS " -Wl,-force_load,${CMAKE_BINARY_DIR}/lib/lean/libLake.a.export -install_name @rpath/libLake_shared.dylib")
  string(APPEND CMAKE_EXE_LINKER_FLAGS " -Wl,-rpath,@executable_path/../lib -Wl,-rpath,@executable_path/../lib/lean")
```

--------------------------------

### Initialize a New Lean 4 Package with Lake

Source: https://github.com/leanprover/lean4/blob/master/stage0/src/lake/README.md

Commands to initialize a new Lean 4 package using Lake. `lake init` sets up a package in the current directory, while `lake new` creates it in a new directory. Both commands generate a standard project structure and initialize a Git repository.

```bash
mkdir hello
cd hello
lake init hello
```

```bash
lake new hello
cd hello
```

--------------------------------

### Add Lean Run Tests

Source: https://github.com/leanprover/lean4/blob/master/src/shell/CMakeLists.txt

Dynamically finds all `.lean` files in the `tests/lean/run` directory and adds a CMake test for each, excluding files starting with `.#`. Each test executes `test_single.sh` in the respective directory with the found Lean file as an argument.

```cmake
file(GLOB LEANRUNTESTS "${LEAN_SOURCE_DIR}/../tests/lean/run/*.lean")
FOREACH(T ${LEANRUNTESTS})
  if(NOT T MATCHES "\\.#")
    GET_FILENAME_COMPONENT(T_NAME ${T} NAME)
    add_test(NAME "leanruntest_${T_NAME}"
             WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean/run"
             COMMAND bash -c "${TEST_VARS} ./test_single.sh ${T_NAME}")
  endif()
ENDFOREACH(T)
```

--------------------------------

### Lean4 Theorem Naming Examples: Int Multiplication

Source: https://github.com/leanprover/lean4/blob/master/doc/std/naming.md

These Lean4 code snippets define theorems about non-zero multiplication for integers, including a biconditional statement. They demonstrate the naming algorithm's application in distinguishing theorems with similar structures but different logical content, emphasizing the inclusion of 'iff' for clarity.

```Lean4
theorem Int.mul_ne_zero {a b : Int} (a0 : a ≠ 0) (b0 : b ≠ 0) : a * b ≠ 0 := sorry
theorem Int.mul_ne_zero_iff {a b : Int} : a * b ≠ 0 ↔ a ≠ 0 ∧ b ≠ 0 := sorry
```

--------------------------------

### Lean 4: Termination by Example

Source: https://github.com/leanprover/lean4/blob/master/doc/std/style.md

Demonstrates the use of `termination_by` and `decreasing_by` keywords in Lean 4 for specifying termination arguments. These keywords help the prover understand why a recursive function will terminate. The associated terms are indented like declaration bodies.

```lean
@[inline] def multiShortOption (handle : Char → m PUnit) (opt : String) : m PUnit := do
  let rec loop (p : String.Pos) := do
    if h : opt.atEnd p then
      return
    else
      handle (opt.get' p h)
      loop (opt.next' p h)
  termination_by opt.utf8ByteSize - p.byteIdx
  decreasing_by
    simp [String.atEnd] at h
    apply Nat.sub_lt_sub_left h
    simp [String.lt_next opt p]
  loop ⟨1⟩
```

```lean
def substrEq (s1 : String) (off1 : String.Pos) (s2 : String) (off2 : String.Pos) (sz : Nat) : Bool :=
  off1.byteIdx + sz ≤ s1.endPos.byteIdx && off2.byteIdx + sz ≤ s2.endPos.byteIdx && loop off1 off2 { byteIdx := off1.byteIdx + sz }
where
  loop (off1 off2 stop1 : Pos) :=
    if _h : off1.byteIdx < stop1.byteIdx then
      let c₁ := s1.get off1
      let c₂ := s2.get off2
      c₁ == c₂ && loop (off1 + c₁) (off2 + c₂) stop1
    else true
  termination_by stop1.1 - off1.1
  decreasing_by
    have := Nat.sub_lt_sub_left _h (Nat.add_lt_add_left c₁.utf8Size_pos off1.1)
    decreasing_tactic
```

```lean
theorem div_add_mod (m n : Nat) : n * (m / n) + m % n = m := by
  rw [div_eq, mod_eq]
  have h : Decidable (0 < n ∧ n ≤ m) := inferInstance
  cases h with
  | isFalse h => simp [h]
  | isTrue h =>
    simp [h]
    have ih := div_add_mod (m - n) n
    rw [Nat.left_distrib, Nat.mul_one, Nat.add_assoc, Nat.add_left_comm, ih, Nat.add_comm, Nat.sub_add_cancel h.2]
decreasing_by apply div_rec_lemma; assumption
```

--------------------------------

### Lean Configuration for Default Targets and Dependencies

Source: https://github.com/leanprover/lean4/blob/master/src/lake/README.md

Shows how to define input files and executables in a Lean configuration file, specifying dependencies using target specifiers and module identifiers.

```lean
package "example"

input_file foo where
  path := "inputs/foo.txt"
  text := true

@[default_target]
lean_exe exe where
  needs := #[`@/foo] -- i.e., `@examole/foo
```

```lean
input_file foo where
  path := "inputs/foo.txt"
  text := true

lean_exe exe where
  needs := #[foo]
```

--------------------------------

### Initialize Lean 4 Package with `lake init`

Source: https://github.com/leanprover/lean4/blob/master/src/lake/README.md

Initializes a new Lean 4 package in the current directory. It sets up the necessary files and directory structure for a Lake-managed project. Requires the package name as an argument.

```bash
mkdir hello
cd hello
lake init hello
```

--------------------------------

### Target Specification Syntax in Lean Literals

Source: https://github.com/leanprover/lean4/blob/master/stage0/src/lake/README.md

Complete literal syntax for target specifiers in Lean configuration files. Backtick-prefixed literals starting with @ for targets or + for modules, optionally including package and facet qualifiers.

```lean
`@[<package>]/[<target>|[+]<module>][:<facet>]
`+<module>[:<facet>]
```

--------------------------------

### Configure Lean Package Tests

Source: https://github.com/leanprover/lean4/blob/master/src/shell/CMakeLists.txt

This setup tests Lean packages. It searches for subdirectories within the `pkg` test directory that contain a `test.sh` script. For each such directory, it adds a test that executes that specific `test.sh` script, allowing for package-level testing.

```cmake
file(GLOB LEANPKGTESTS "${LEAN_SOURCE_DIR}/../tests/pkg/*")
FOREACH(T ${LEANPKGTESTS})
  if(EXISTS ${T}/test.sh)
    GET_FILENAME_COMPONENT(T_NAME ${T} NAME)
    add_test(NAME "leanpkgtest_${T_NAME}"
            WORKING_DIRECTORY "${T}"
            COMMAND bash -c "${TEST_VARS} ./test.sh")
  endif()
ENDFOREACH(T)
```

--------------------------------

### Lean4 Theorem Naming Example: List IsPrefix

Source: https://github.com/leanprover/lean4/blob/master/doc/std/naming.md

This Lean4 code snippet showcases a theorem related to List.IsPrefix, specifically concerning the head element of lists. It's used to illustrate the naming algorithm's application, particularly how namespaces and specific properties influence the name.

```Lean4
example {x y : List α} (h : x <+: y) (hx : x ≠ []) :
  x.head hx = y.head (h.ne_nil hx) := sorry
```

--------------------------------

### Initialize Lean Runtime and Modules (C/C++)

Source: https://github.com/leanprover/lean4/blob/master/doc/dev/ffi.md

Demonstrates the C/C++ code required to initialize the Lean runtime and specific modules. It includes essential functions like `lean_initialize_runtime_module`, `lean_initialize`, `lean_setup_args`, and module-specific initializers. Proper handling of initialization results and process arguments is crucial.

```c
void lean_initialize_runtime_module();
void lean_initialize();
char ** lean_setup_args(int argc, char ** argv);

lean_object * initialize_A_B(uint8_t builtin);
lean_object * initialize_C(uint8_t builtin);
...

argv = lean_setup_args(argc, argv); // if using process-related functionality
lean_initialize_runtime_module();
//lean_initialize();  // necessary (and replaces `lean_initialize_runtime_module`) if you (indirectly) access the `Lean` package

lean_object * res;
// use same default as for Lean executables
uint8_t builtin = 1;
res = initialize_A_B(builtin);
if (lean_io_result_is_ok(res)) {
    lean_dec_ref(res);
} else {
    lean_io_result_show_error(res);
    lean_dec(res);
    return ...;  // do not access Lean declarations if initialization failed
}
res = initialize_C(builtin);
if (lean_io_result_is_ok(res)) {
...

//lean_init_task_manager();  // necessary if you (indirectly) use `Task`
lean_io_mark_end_initialization();
```

--------------------------------

### Lean 4 `do` Notation: Modifying Meta-Context

Source: https://github.com/leanprover/lean4/blob/master/doc/std/style.md

Demonstrates advanced usage of `do` notation in Lean 4 for manipulating the meta-context. This example involves iterating through goals, checking for anonymous metavariables, and updating their names based on provided tags and suffixes.

```Lean
def tagUntaggedGoals (parentTag : Name) (newSuffix : Name) (newGoals : List MVarId) : TacticM Unit := do
  let mctx ← getMCtx
  let mut numAnonymous := 0
  for g in newGoals do
    if mctx.isAnonymousMVar g then
      numAnonymous := numAnonymous + 1
  modifyMCtx fun mctx => Id.run do
    let mut mctx := mctx
    let mut idx  := 1
    for g in newGoals do
      if mctx.isAnonymousMVar g then
        if numAnonymous == 1 then
          mctx := mctx.setMVarUserName g parentTag
        else
          mctx := mctx.setMVarUserName g (parentTag ++ newSuffix.appendIndexAfter idx)
        idx := idx + 1
    pure mctx
```

--------------------------------

### Build and Run Cross Benchmark Suite with Nix and Make

Source: https://github.com/leanprover/lean4/blob/master/tests/bench/README.md

Builds and runs the heavy-weight Cross benchmark suite. This process is recommended to be performed using Nix for reproducible builds. It records multiple runs, generates CSV and HTML reports, and prints tabulated results to stdout.

```shell
nix develop
make
```

--------------------------------

### Defining Lean Libraries in Lean and TOML

Source: https://github.com/leanprover/lean4/blob/master/src/lake/README.md

Illustrates the syntax for defining a Lean library target in both Lean configuration files and TOML configuration files.

```lean
lean_lib «target-name» where
  -- configuration options go here
```

```toml
[[lean_lib]]
name = "«target-name»"
```

--------------------------------

### Find LibUV on Native Platforms

Source: https://github.com/leanprover/lean4/blob/master/stage0/src/CMakeLists.txt

This snippet demonstrates how to find and use the LibUV library on native platforms when not building for Emscripten. It uses CMake's `find_package` command to locate an installed version of LibUV (version 1.0.0 or higher). The include directories and linker flags are then made available for use in the project.

```cmake
else()
  find_package(LibUV 1.0.0 REQUIRED)
endif()
include_directories(${LIBUV_INCLUDE_DIRS})
if(NOT LEAN_STANDALONE)
  string(JOIN " " LIBUV_LDFLAGS ${LIBUV_LDFLAGS})
  string(APPEND LEAN_EXTRA_LINKER_FLAGS " ${LIBUV_LDFLAGS}")
endif()
```

--------------------------------

### Create Lean 4 Package with `lake new`

Source: https://github.com/leanprover/lean4/blob/master/src/lake/README.md

Creates a new Lean 4 package in a new directory. This command also initializes a Git repository and sets up the standard Lake project structure. Requires the package name as an argument.

```bash
lake new hello
cd hello
```

--------------------------------

### CMake: Feature Options Configuration

Source: https://github.com/leanprover/lean4/blob/master/src/CMakeLists.txt

Defines several boolean options to control project features. These include multi-threading, CCACHE usage, LLVM support, version string inclusion of git hash, installation of license files and cadical, and various optimization and debugging related flags.

```cmake
option(MULTI_THREAD       "MULTI_THREAD"       ON)
option(CCACHE             "use ccache"         ON)
option(SPLIT_STACK        "SPLIT_STACK"        OFF)
# When OFF we disable LLVM support
option(LLVM               "LLVM"               OFF)

# When ON we include githash in the version string
option(USE_GITHASH        "GIT_HASH"           ON)
# When ON we install LICENSE files to CMAKE_INSTALL_PREFIX
option(INSTALL_LICENSE "INSTALL_LICENSE" ON)
# When ON we install a copy of cadical
option(INSTALL_CADICAL "Install a copy of cadical" ON)

# FLAGS for disabling optimizations and debugging
option(FREE_VAR_RANGE_OPT  "FREE_VAR_RANGE_OPT"   ON)
option(HAS_LOCAL_OPT       "HAS_LOCAL_OPT"        ON)
option(ABSTRACTION_CACHE   "ABSTRACTION_CACHE"    ON)
option(TYPE_CLASS_CACHE    "TYPE_CLASS_CACHE"     ON)
option(TYPE_INFER_CACHE    "TYPE_INFER_CACHE"     ON)
option(ALPHA               "ALPHA FEATURES"       OFF)
option(TRACK_CUSTOM_ALLOCATORS "TRACK_CUSTOM_ALLOCATORS" OFF)
option(TRACK_LIVE_EXPRS    "TRACK_LIVE_EXPRS" OFF)
option(CUSTOM_ALLOCATORS   "CUSTOM_ALLOCATORS" ON)
option(SAVE_SNAPSHOT       "SAVE_SNAPSHOT" ON)
option(SAVE_INFO           "SAVE_INFO" ON)
option(SMALL_ALLOCATOR     "SMALL_ALLOCATOR" OFF)
option(MMAP                "MMAP" ON)
option(LAZY_RC             "LAZY_RC" OFF)
option(RUNTIME_STATS       "RUNTIME_STATS" OFF)
option(BSYMBOLIC "Link with -Bsymbolic to reduce call overhead in shared libraries (Linux)" ON)
option(USE_GMP "USE_GMP" ON)
option(USE_MIMALLOC "use mimalloc" ON)
```

--------------------------------

### TOML Configuration for Lean Libraries and Executables

Source: https://github.com/leanprover/lean4/blob/master/src/lake/README.md

Demonstrates how to define Lean libraries and executables within a TOML configuration file, including specifying plugin dependencies.

```toml
name = "example"

[[lean_lib]]
name = "Plugin"

[[lean_exe]]
name = "exe"
plugins = ["Plugin:shared"] # i.e., @example/Plugin:shared
```

--------------------------------

### Configuring Lean Version and Build Options

Source: https://github.com/leanprover/lean4/blob/master/stage0/src/CMakeLists.txt

Configures Lean's version and build-related header files. It copies version information and sets a macro (LEAN_IS_STAGE0) indicating if it's a stage 0 build. It also conditionally includes mimalloc headers if USE_MIMALLOC is enabled and installs generated headers and build scripts.

```cmake
# Version
configure_file("${LEAN_SOURCE_DIR}/version.h.in" "${LEAN_BINARY_DIR}/include/lean/version.h")
if (${STAGE} EQUAL 0)
  set(LEAN_IS_STAGE0 "#define LEAN_IS_STAGE0 1")
else()
  set(LEAN_IS_STAGE0 "#define LEAN_IS_STAGE0 0")
endif()
configure_file("${LEAN_SOURCE_DIR}/config.h.in" "${LEAN_BINARY_DIR}/include/lean/config.h")
if (USE_MIMALLOC)
  file(COPY "${LEAN_BINARY_DIR}/../mimalloc/src/mimalloc/include/mimalloc.h" DESTINATION "${LEAN_BINARY_DIR}/include/lean")
endif()
install(DIRECTORY ${LEAN_BINARY_DIR}/include/ DESTINATION include)
configure_file(${LEAN_SOURCE_DIR}/lean.mk.in ${LEAN_BINARY_DIR}/share/lean/lean.mk)
install(DIRECTORY ${LEAN_BINARY_DIR}/share/ DESTINATION share)
```

--------------------------------

### Lean 4 Structure: Subarray

Source: https://github.com/leanprover/lean4/blob/master/doc/style.md

Defines a 'Subarray' structure representing a slice of an 'Array'. It includes the underlying 'array', the 'start' index (inclusive), the 'stop' index (exclusive), and proofs that 'start <= stop' and 'stop' is within the array bounds.

```lean
/--
A section or “slice” of an array that shares the underlying memory allocation.

Subarrays can be used to avoid unnecessary copying and allocation of arrays. However,
subarrays retain a reference to their underlying array. The existence of multiple
subarrays from the same array will thus prevent array operations from being optimized
into mutation, even if the subarrays are disjoint.
-/
structure Subarray (α : Type u) where
  /--
  The underlying array.
  -/ 
  array : Array α
  /--
  The first index in the subarray, inclusive.
  -/ 
  start : Nat
  /--
  The last index in the subarray, exclusive.
  -/ 
  stop : Nat
  /--
  The start of the subarray is not greater than the end.
  -/ 
  start_le_stop : start ≤ stop
  /--
  The end of the subarray is within bounds for the underlying array.
  -/ 
  stop_le_array_size : stop ≤ array.size
```

--------------------------------

### Multi-line Term Splitting in Lean 4

Source: https://github.com/leanprover/lean4/blob/master/doc/std/style.md

Illustrates how to split complex Lean 4 terms across multiple lines, focusing on increasing indentation, splitting at argument boundaries, and handling infix operators. It provides examples for function applications, if-then-else expressions, and comma-separated bracketed sequences.

```Lean
theorem eraseP_eq_iff {
  p : α → Bool
  l : List α
} :
    l.eraseP p = l' ↔
      ((∀ a ∈ l, ¬ p a) ∧ l = l') ∨
        ∃ a l₁ l₂,
          (∀ b ∈ l₁, ¬ p b) ∧ p a ∧
          l = l₁ ++ a :: l₂ ∧ l' = l₁ ++ l₂ :=
  sorry

theorem size_alter [LawfulBEq α] {k : α} {f : Option (β k) → Option (β k)} (h : m.WF) :
    (m.alter k f).size = 
      if m.contains k && (f (m.get? k)).isNone then
        m.size - 1
      else if !m.contains k && (f (m.get? k)).isSome then
        m.size + 1
      else
        m.size :=
  by simp_to_raw using Raw₀.size_alter

example : Nat × Nat :=
  ⟨imagineThisWasALongTerm,
    imagineThisWasAnotherLongTerm⟩

```

--------------------------------

### Add Lean Executable Help Tests

Source: https://github.com/leanprover/lean4/blob/master/src/shell/CMakeLists.txt

Adds CMake tests to verify the Lean executable's `--help` and `-h` options, ensuring the command-line interface functions correctly.

```cmake
add_test(lean_help1    "${CMAKE_BINARY_DIR}/bin/lean" --help)
add_test(lean_help2    "${CMAKE_BINARY_DIR}/bin/lean" -h)
```

--------------------------------

### Build Lake from Source using Shell Script

Source: https://github.com/leanprover/lean4/blob/master/src/lake/README.md

Instructions for building the Lake executable from its source code using a provided `build.sh` script. This script passes arguments to `make`, allowing for parallel build tasks using the `-jX` option. The resulting binary is placed in `.lake/build/bin/lake`.

```shell
#!/bin/sh

# Example usage:
# ./build.sh -j4
```

--------------------------------

### Run Lean 4 Test Suite

Source: https://github.com/leanprover/lean4/blob/master/doc/dev/testing.md

Executes the full Lean 4 test suite using `make test` after building. Allows specifying the number of parallel test jobs.

```bash
cd build/release
make test ARGS=-j4
```

--------------------------------

### Git Commit Message Example with C++ Code Block

Source: https://github.com/leanprover/lean4/blob/master/doc/dev/commit_convention.md

Complete example of a commit message following the convention. Demonstrates the fix type with a detailed body explaining the motivation for adding operator<< declarations in the kernel to prevent silent type coercion issues. Includes a C++ code block illustrating the problem being solved.

```text
fix: add declarations for operator<<(std::ostream&, expr const&) and operator<<(std::ostream&, context const&) in the kernel

This PR adds declarations `operator<<` for raw printing.
The actual implementation of these two operators is outside of the
kernel. They are implemented in the file 'library/printer.cpp'.

We declare them in the kernel to prevent the following problem.
Suppose there is a file 'foo.cpp' that does not include 'library/printer.h',
but contains
```cpp
expr a;
...
std::cout << a << "\n";
...
```

The compiler does not generate an error message. It silently uses the
operator bool() to coerce the expression into a Boolean. This produces
counter-intuitive behavior, and may confuse developers.
```

--------------------------------

### Supported Dependency Sources in Lean `require`

Source: https://github.com/leanprover/lean4/blob/master/stage0/src/lake/README.md

Illustrates the `from` clause syntax for specifying dependency sources in Lean Lake. Supports direct paths for local packages and Git URLs with optional revisions and subdirectories.

```Lean
# Path Dependencies
from <path>

# Git Dependencies
from git <url> [@ <rev>] [/ <subDir>]
```

--------------------------------

### Get standard input stream - IO operation in Lean

Source: https://github.com/leanprover/lean4/blob/master/doc/style.md

Returns the current thread's standard input stream. This opaque function demonstrates documentation for external I/O operations that can be replaced using IO.setStdin.

```lean
@[extern "lean_get_stdin"] opaque getStdin  : BaseIO FS.Stream
```

--------------------------------

### Define Lean Library Target in Lean

Source: https://github.com/leanprover/lean4/blob/master/stage0/src/lake/README.md

Create a Lean library target in lakefile.lean configuration. Lean libraries define sets of modules available for import and specify build configuration options.

```lean
lean_lib «target-name» where
  -- configuration options go here
```

--------------------------------

### Find Python Interpreter

Source: https://github.com/leanprover/lean4/blob/master/stage0/src/CMakeLists.txt

This CMake command finds the Python interpreter. This is a standard CMake function used to locate Python installations on the system, typically for use in build scripts or by dependent projects.

```cmake
# Python
find_package(PythonInterp)
```