### NatOrInt Evaluation Example

Source: https://lean-lang.org/doc/reference/latest/Interacting-with-Lean

Example usage of the NatOrInt Repr instance.

```lean
open NatOrInt in `(NatOrInt.nat (3)) (NatOrInt.int (5)) (NatOrInt.int (-5)) `#eval do IO.println <| repr <| nat 3 IO.println <| repr <| int 5 IO.println <| repr <| int (-5) 
```

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

### Axiom and Stuck Reduction Example

Source: https://lean-lang.org/doc/reference/latest/Axioms

Demonstrates how adding an axiom like `Nat.otherZero` can cause definitional reductions to get stuck, preventing further progress with `Nat.rec`.

```Lean
axiom Nat.otherZero : Nat 
((Nat.rec ⟨fun x => x, PUnit.unit⟩ (fun n n_ih => ⟨fun x => (n_ih.1 x).succ, n_ih⟩) Nat.otherZero).1 4).succ.succ
```

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

### Basic #guard_msgs Example

Source: https://lean-lang.org/doc/reference/latest/Interacting-with-Lean

Captures all messages from the `example` command and checks if they match the docstring, which expects an 'error: Unknown identifier `x`'. This consumes the message.

```lean
/--
error: Unknown identifier `x`
-/ 
#guard_msgs in
example : α := x

```

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

### Example of Std.Format.align

Source: https://lean-lang.org/doc/reference/latest/Interacting-with-Lean

Demonstrates the usage of Std.Format.align with nesting and newlines.

```Lean
open Std Format in
#eval IO.println (nest 2 <| "." ++ align ++ "a" ++ line ++ "b")
```

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

### Example of Std.Format.nest

Source: https://lean-lang.org/doc/reference/latest/Interacting-with-Lean

Illustrates how Std.Format.nest is used with a list of formats to create indented, potentially multi-line output.

```Lean
open Std Format in def fmtList (l : List Format) : Format := let f := joinSep l (", " ++ Format.line) group (nest 1 <| "[" ++ f ++ "]") 
```

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

### Basic Guard Messages Example

Source: https://lean-lang.org/doc/reference/latest/Interacting-with-Lean

This example demonstrates the basic usage of `#guard_msgs` to check for a specific error message. It captures all messages generated by the `example` command and asserts that an 'Unknown identifier `x`' error is present.

```lean
/--
error: Unknown identifier `x`
-/
#guard_msgs in
example : α := x

```

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

### Namespace Opening and Scoping Examples

Source: https://lean-lang.org/doc/reference/latest/Namespaces-and-Sections

Demonstrates basic namespace opening, scoped opening, hiding, and renaming definitions within Lean sections.

```lean
/-- SKI combinators https://en.wikipedia.org/wiki/SKI_combinator_calculus -/
namespace Combinator.Calculus
  def I (a : α) : α := a
  def K (a : α) : β → α := fun _ => a
  def S (x : α → β → γ) (y : α → β) (z : α) : γ := x z (y z)
end Combinator.Calculus

section
  -- open everything under `Combinator.Calculus`, *i.e.* `I`, `K` and `S`,
  -- until the section ends
  open Combinator.Calculus

  theorem SKx_eq_K : S K x = I := rfl
end

-- open everything under `Combinator.Calculus` only for the next command (the next `theorem`, here)
open Combinator.Calculus in
theorem SKx_eq_K' : S K x = I := rfl

section
  -- open only `S` and `K` under `Combinator.Calculus`
  open Combinator.Calculus (S K)

  theorem SKxy_eq_y : S K x y = y := rfl

  -- `I` is not in scope, we have to use its full path
  theorem SKxy_eq_Iy : S K x y = Combinator.Calculus.I y := rfl
end

section
  open Combinator.Calculus
    renaming
      I → identity,
      K → konstant

  #check identity
  #check konstant
end

section
  open Combinator.Calculus
    hiding S

  #check I
  #check K
end

section
  namespace Demo
    inductive MyType
    | val

    namespace N1
      scoped infix:68 " ≋ " => BEq.beq

      scoped instance : BEq MyType where
        beq _ _ := true

      def Alias := MyType
    end N1
  end Demo

  -- bring `≋` and the instance in scope, but not `Alias`
  open scoped Demo.N1

  #check Demo.MyType.val == Demo.MyType.val
  #check Demo.MyType.val ≋ Demo.MyType.val
  -- #check Alias -- unknown identifier 'Alias'
end
```

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

### Basic Guard Messages Example

Source: https://lean-lang.org/doc/reference/latest/Interacting-with-Lean

This example captures messages generated by a command and checks them against the docstring content. It ensures an 'Unknown identifier `x`' error is present and then consumes the message.

```lean
/-- error: Unknown identifier `x` -/ #guard_msgs in example : α := x
```

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

### Print Axioms for a Specific Function in Lean

Source: https://lean-lang.org/doc/reference/latest/Interacting-with-Lean

This example shows the axioms used by the 'swap_eq_swap'' theorem, including one generated by 'bv_decide'.

```Lean
#print axioms swap_eq_swap'
```

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

### Demonstrate Decimal Coercion to Nat and Int

Source: https://lean-lang.org/doc/reference/latest/Coercions

This example demonstrates coercing `Decimal` values to both `Nat` and `Int` to show how coercions can be chained or applied in different contexts.

```Lean
def twoHundredThirteen : Decimal where digits := #[2, 1, 3] 
def one : Decimal where digits := #[1] 
#eval (one : Int) - (twoHundredThirteen : Nat)
```

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

### Basic #guard_msgs Example

Source: https://lean-lang.org/doc/reference/latest/Interacting-with-Lean

Captures messages generated by a command and checks that they match the docstring content. This example checks for an 'Unknown identifier' error.

```lean
/--
error: Unknown identifier `x`
-/
#guard_msgs in
example : α := x
```

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

### Custom Repr Instance for Inductive Types (Example)

Source: https://lean-lang.org/doc/reference/latest/Interacting-with-Lean

Example of a custom Repr instance for the `NatOrInt` inductive type, following Lean's conventions for precedence, naming, nesting, and formatting.

```APIDOC
## Custom Repr Instance for Inductive Types (Example)

### Description
This example demonstrates how to write a custom `Repr` instance for an inductive type like `N.NatOrInt`. It adheres to the conventions of using `Repr.addAppParen`, `group`, `nestD`, `line`, and `max_prec` for proper formatting and precedence handling.

### Method
`instance : Repr NatOrInt`

### Endpoint
N/A (This is a typeclass instance definition)

### Parameters
N/A (Instance definition)

### Request Body
N/A (Instance definition)

### Request Example
```lean
namespace N
inductive NatOrInt where
  | nat : Nat → NatOrInt
  | int : Int → NatOrInt

instance : Repr NatOrInt where
  reprPrec n prec :=
    match n with
    | .nat nat_val =>
      Repr.addAppParen <| .group <| .nestD <| "N.NatOrInt.nat" ++ .line ++ reprPrec nat_val max_prec
    | .int int_val =>
      Repr.addAppParen <| .group <| .nestD <| "N.NatOrInt.int" ++ .line ++ reprPrec int_val max_prec
```

### Response
#### Success Response (Formatted String)
- **Formatted String**: The string representation of a `NatOrInt` value, correctly formatted according to the defined `Repr` instance.

#### Response Example
```lean
#eval IO.println (repr (NatOrInt.nat 5))
-- Output: N.NatOrInt.nat 5

#eval IO.println (repr (NatOrInt.int (-5)))
-- Output: N.NatOrInt.int (-5)

#eval IO.println (repr <| (List.range 10).map (NatOrInt.nat))
-- Output:
-- [
--  N.NatOrInt.nat 0,
--  N.NatOrInt.nat 1,
--  N.NatOrInt.nat 2,
--  N.NatOrInt.nat 3,
--  N.NatOrInt.nat 4,
--  N.NatOrInt.nat 5,
--  N.NatOrInt.nat 6,
--  N.NatOrInt.nat 7,
--  N.NatOrInt.nat 8,
--  N.NatOrInt.nat 9
-- ]
```
```

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

### Evaluate format expressions

Source: https://lean-lang.org/doc/reference/latest/Interacting-with-Lean

Examples of evaluating format expressions in the Lean environment.

```lean
#eval nums
```

```lean
#eval IO.println (pretty (parenSeq nums))
```

```lean
#eval IO.println (pretty grouped)
```

```lean
#eval IO.println (pretty filled)
```

```lean
#eval IO.println (pretty (width := 30) grouped)
```

```lean
#eval IO.println (pretty (width := 30) filled)
```

```lean
#eval IO.println <| pretty (width := 30) (fill (parenSeq (nums ++ nums ++ nums ++ nums)))
```

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

### Password Access Control with Exceptions

Source: https://lean-lang.org/doc/reference/latest/IO/Logical-Model

This example demonstrates using exceptions for control flow in the IO monad. It repeatedly prompts for a password, throwing an error for incorrect attempts and proceeding on success. Any unhandled exceptions are re-thrown.

```lean
def accessControl : IO Unit :=
  do
    IO.println "What is the password?"
    password ← (← IO.getStdin).getLine
    if password.trimAscii.copy != "secret" then
      throw (.userError "Incorrect password")
    else
      return ()
```

```lean
def repeatAccessControl : IO Unit :=
  do
    repeat
      try
        accessControl
      break
      catch
      | .userError "Incorrect password" => continue
      | other => throw other
```

```lean
def main : IO Unit :=
  do
    repeatAccessControl
    IO.println "Access granted!"
```

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

### Print Axioms Used by a Theorem in Lean

Source: https://lean-lang.org/doc/reference/latest/Axioms

Combine `#print axioms` with `#guard_msgs` to verify that a theorem does not introduce new dependencies on axioms. This example checks the `double_neg_elim` theorem.

```lean
theorem double_neg_elim (P : Prop) : (¬ ¬ P) = P := propext Classical.not_not /-- info: 'double_neg_elim' depends on axioms:   [propext, Classical.choice, Quot.sound] -/ #guard_msgs (whitespace := lax) in #print axioms double_neg_elim
```

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

### Define basic coercions in Lean

Source: https://lean-lang.org/doc/reference/latest/Coercions

Examples of standard library coercions including Nat to Int, Fin to Nat, and wrapping values in Option or Thunk.

```lean
example (n : Nat) : Int := n example (n : Fin k) : Nat := n example (x : α) : Option α := x def th (f : Int → String) (x : Nat) : Thunk String := f x open Lean in example (n : Ident) : Term := n
```

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

### Custom Repr Instance for NatOrInt in Lean

Source: https://lean-lang.org/doc/reference/latest/Interacting-with-Lean

An example of a custom `Repr` instance for the `NatOrInt` inductive type. It follows conventions for precedence, grouping, indentation, and line breaks, demonstrating how to represent `Nat` and `Int` variants.

```lean
instance : Repr NatOrInt where
  reprPrec | .nat n => Repr.addAppParen <| .group <| .nestD <| "N.NatOrInt.nat" ++ .line ++ reprPrec n max_prec
  | .int i => Repr.addAppParen <| .group <| .nestD <| "N.NatOrInt.int" ++ .line ++ reprPrec i max_prec
```

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

### Example of LengthList with correct types

Source: https://lean-lang.org/doc/reference/latest/The-Type-System

Demonstrates the correct usage of `LengthList` with `Int` and `String` types for lengths 0 and 2 respectively. Note that Lean's tuples nest to the right, so explicit parentheses are not always needed.

```Lean
example : LengthList Int 0 := ()
```

```Lean
example : LengthList String 2 := ("Hello", "there", ()) 
```

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

### Get' Function

Source: https://lean-lang.org/doc/reference/latest/the-index

Documentation for the 'get'' function, likely a variant of 'get'.

```APIDOC
## Get' Function

### Description
A variant of the 'get' function, possibly with different error handling or behavior.

### Endpoint
- `String.Pos.Raw.get'`

### Usage
This function is used for retrieving characters or elements with a specific behavior defined by `String.Pos.Raw`.
```

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

### Get Functions (Various Types)

Source: https://lean-lang.org/doc/reference/latest/the-index

Details on the 'get' function for accessing elements, across multiple data types and modules.

```APIDOC
## Get Functions (Various Types)

### Description
The `get` function retrieves an element from a collection or structure. Variants exist for different data types and contexts, including state monads.

### Endpoints
- `ByteArray.get`
- `ByteSlice.get`
- `EStateM.get`
- `List.get`
- `MonadState.get`
- `MonadStateOf.get` (class method)
- `Option.get`
- `ST.Ref.get`
- `StateRefT'.get`
- `StateT.get`
- `Std.DHashMap.get`
- `Std.DTreeMap.get`
- `Std.ExtDHashMap.get`
- `Std.ExtHashMap.get`
- `Std.ExtHashSet.get`
- `Std.HashMap.get`
- `Std.HashSet.get`
- `Std.TreeMap.get`
- `Std.TreeSet.get`
- `String.Pos.Raw.get`
- `String.Pos.get`
- `String.Slice.Pos.get`
- `Subarray.get`
- `Substring.Raw.get`
- `Task.get`
- `Thunk.get`

### Usage
This is a fundamental function for accessing data. The specific behavior depends on the type it's applied to, ranging from array indexing to state retrieval in monads.
```

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

### Get! Functions (Various Types)

Source: https://lean-lang.org/doc/reference/latest/the-index

Details on the 'get!' function for accessing elements that are guaranteed to exist, across multiple data types.

```APIDOC
## Get! Functions (Various Types)

### Description
The `get!` function is used to retrieve an element from a collection or structure, raising an error if the element is not found. It is assumed the element exists.

### Endpoints
- `ByteArray.get!`
- `ByteSlice.get!`
- `Option.get!`
- `Std.DHashMap.get!`
- `Std.DTreeMap.get!`
- `Std.ExtDHashMap.get!`
- `Std.ExtHashMap.get!`
- `Std.ExtHashSet.get!`
- `Std.HashMap.get!`
- `Std.HashSet.get!`
- `Std.TreeMap.get!`
- `Std.TreeSet.get!`
- `String.Pos.Raw.get!`
- `String.Pos.get!`
- `String.Slice.Pos.get!`
- `Subarray.get!`

### Usage
Use `get!` when you are certain an element exists at a given position or key to avoid runtime errors associated with optional types.
```

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

### Get? Functions (Various Types)

Source: https://lean-lang.org/doc/reference/latest/the-index

Details on the 'get?' function for safely accessing elements that might not exist, across multiple data types.

```APIDOC
## Get? Functions (Various Types)

### Description
The `get?` function attempts to retrieve an element from a collection or structure, returning an option type (e.g., `Option.some` or `Option.none`) if the element is not found. This provides a safe way to access potentially missing elements.

### Endpoints
- `Std.DHashMap.get?`
- `Std.DTreeMap.get?`
- `Std.ExtDHashMap.get?`
- `Std.ExtHashMap.get?`
- `Std.ExtHashSet.get?`
- `Std.HashMap.get?`
- `Std.HashSet.get?`
- `Std.TreeMap.get?`
- `Std.TreeSet.get?`
- `String.Pos.Raw.get?`
- `String.Pos.get?`
- `String.Slice.Pos.get?`

### Usage
Use `get?` when there's a possibility that an element might not exist at the specified location or key. It helps in writing robust code by explicitly handling the case of missing elements.
```

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

### General configuration syntax

Source: https://lean-lang.org/doc/reference/latest/Interacting-with-Lean

Shows the general syntax for providing multiple configuration clauses to #guard_msgs.

```lean
#guard_msgs (configElt,*) in cmd
```

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

### BEq and BEq.mk

Source: https://lean-lang.org/doc/reference/latest/the-index

Documentation for the BEq type and its instance constructor.

```APIDOC
## BEq and BEq.mk

### Description
Documentation for the BEq type and its instance constructor.

### Method
N/A

### Endpoint
N/A

### Parameters
N/A

### Request Example
N/A

### Response
#### Success Response (200)
N/A

#### Response Example
N/A
```

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

### Build a Lean Module

Source: https://lean-lang.org/doc/reference/latest/ValidatingProofs

Use the Lake build tool to verify a module from the command line, ensuring all proofs are checked without relying on editor-specific UI.

```bash
lake build +Module
```

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

### Lean Command Syntax for Definitions

Source: https://lean-lang.org/doc/reference/latest/Definitions/Definitions

Illustrates the general syntax for Lean commands, including definitions with modifiers, identifiers, and optional signatures. Modifiers like doc comments, attributes, visibility, and termination hints are explained.

```lean
command ::= ...
    | 
declModifiers is the collection of modifiers on a declaration:



  * a doc comment /-- ... -/


  * a list of attributes @[attr1, attr2]


  * a visibility specifier, private or public


  * protected


  * noncomputable


  * unsafe


  * partial or nonrec



All modifiers are optional, and have to come in the listed order.


nestedDeclModifiers is the same as declModifiers, but attributes are printed
on the same line as the declaration. It is used for declarations nested inside other syntax,
such as inductive constructors, structure projections, and let rec / where definitions.


declModifiers
      def 
declId matches foo or foo.{u,v}: an identifier possibly followed by a list of universe names 

declId 
optDeclSig matches the signature of a declaration with optional type: a list of binders and then possibly : type 

optDeclSig := term
Termination hints are termination_by and decreasing_by, in that order.
```

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

### I Functions

Source: https://lean-lang.org/doc/reference/latest/the-index

Functions starting with the letter 'I'.

```APIDOC
## is­Finite

### Description
Checks if a float is finite.

### Method
N/A (Function/Method Call)

### Endpoint
N/A

### Parameters
None

### Request Example
None

### Response
None

## is­GE

### Description
Checks if the ordering is greater than or equal to.

### Method
N/A (Function/Method Call)

### Endpoint
N/A

### Parameters
None

### Request Example
None

### Response
None

## is­GT

### Description
Checks if the ordering is greater than.

### Method
N/A (Function/Method Call)

### Endpoint
N/A

### Parameters
None

### Request Example
None

### Response
None

## is­Inf

### Description
Checks if a float is infinity.

### Method
N/A (Function/Method Call)

### Endpoint
N/A

### Parameters
None

### Request Example
None

### Response
None

## is­Int

### Description
Checks if a string represents an integer.

### Method
N/A (Function/Method Call)

### Endpoint
N/A

### Parameters
None

### Request Example
None

### Response
None

## is­LE

### Description
Checks if the ordering is less than or equal to.

### Method
N/A (Function/Method Call)

### Endpoint
N/A

### Parameters
None

### Request Example
None

### Response
None

## is­LT

### Description
Checks if the ordering is less than.

### Method
N/A (Function/Method Call)

### Endpoint
N/A

### Parameters
None

### Request Example
None

### Response
None

## is­Left

### Description
Checks if a Sum type is the Left variant.

### Method
N/A (Function/Method Call)

### Endpoint
N/A

### Parameters
None

### Request Example
None

### Response
None

## is­Lower

### Description
Checks if a character is lowercase.

### Method
N/A (Function/Method Call)

### Endpoint
N/A

### Parameters
None

### Request Example
None

### Response
None

## is­Lt

### Description
Checks if a Fin value is less than.

### Method
N/A (Function/Method Call)

### Endpoint
N/A

### Parameters
None

### Request Example
None

### Response
None

## is­Na­N

### Description
Checks if a float is Not a Number (NaN).

### Method
N/A (Function/Method Call)

### Endpoint
N/A

### Parameters
None

### Request Example
None

### Response
None

## is­Nat

### Description
Checks if a string or substring represents a natural number.

### Method
N/A (Function/Method Call)

### Endpoint
N/A

### Parameters
None

### Request Example
None

### Response
None

## is­Ne

### Description
Checks if the ordering is not equal.

### Method
N/A (Function/Method Call)

### Endpoint
N/A

### Parameters
None

### Request Example
None

### Response
None

## is­Nil

### Description
Checks if a format is nil.

### Method
N/A (Function/Method Call)

### Endpoint
N/A

### Parameters
None

### Request Example
None

### Response
None

## is­None

### Description
Checks if an Option is None.

### Method
N/A (Function/Method Call)

### Endpoint
N/A

### Parameters
None

### Request Example
None

### Response
None

## is­OSX

### Description
Checks if the current platform is macOS.

### Method
N/A (Function/Method Call)

### Endpoint
N/A

### Parameters
None

### Request Example
None

### Response
None

## is­Of­Kind

### Description
Checks if a syntax element is of a specific kind.

### Method
N/A (Function/Method Call)

### Endpoint
N/A

### Parameters
None

### Request Example
None

### Response
None

## is­Ok

### Description
Checks if an Except type is Ok.

### Method
N/A (Function/Method Call)

### Endpoint
N/A

### Parameters
None

### Request Example
None

### Response
None

## is­Perm

### Description
Checks if a list is a permutation of another list.

### Method
N/A (Function/Method Call)

### Endpoint
N/A

### Parameters
None

### Request Example
None

### Response
None

## is­Power­Of­Two

### Description
Checks if a natural number is a power of two.

### Method
N/A (Function/Method Call)

### Endpoint
N/A

### Parameters
None

### Request Example
None

### Response
None

## is­Prefix­Of

### Description
Checks if a list or string is a prefix of another.

### Method
N/A (Function/Method Call)

### Endpoint
N/A

### Parameters
None

### Request Example
None

### Response
None

## is­Prefix­Of?

### Description
Checks if a list is a prefix of another (possibly with different types).

### Method
N/A (Function/Method Call)

### Endpoint
N/A

### Parameters
None

### Request Example
None

### Response
None

## is­Relative

### Description
Checks if a file path is relative.

### Method
N/A (Function/Method Call)

### Endpoint
N/A

### Parameters
None

### Request Example
None

### Response
None

## is­Resolved

### Description
Checks if a promise has been resolved.

### Method
N/A (Function/Method Call)

### Endpoint
N/A

### Parameters
None

### Request Example
None

### Response
None

## is­Right

### Description
Checks if a Sum type is the Right variant.

### Method
N/A (Function/Method Call)

### Endpoint
N/A

### Parameters
None

### Request Example
None

### Response
None

## is­Some

### Description
Checks if an Option is Some.

### Method
N/A (Function/Method Call)

### Endpoint
N/A

### Parameters
None

### Request Example
None

### Response
None

## is­Some_succ?

### Description
Checks if a PRange is Some and its successor.

### Method
N/A (Function/Method Call)

### Endpoint
N/A

### Parameters
None

### Request Example
None

### Response
None

## is­Sublist

### Description
Checks if a list is a sublist of another.

### Method
N/A (Function/Method Call)

### Endpoint
N/A

### Parameters
None

### Request Example
None

### Response
None

## is­Suffix­Of

### Description
Checks if a list is a suffix of another.

### Method
N/A (Function/Method Call)

### Endpoint
N/A

### Parameters
None

### Request Example
None

### Response
None

## is­Suffix­Of?

### Description
Checks if a list is a suffix of another (possibly with different types).

### Method
N/A (Function/Method Call)

### Endpoint
N/A

### Parameters
None

### Request Example
None

### Response
None

## is­Tty

### Description
Checks if a file handle or stream is a TTY.

### Method
N/A (Function/Method Call)

### Endpoint
N/A

### Parameters
None

### Request Example
None

### Response
None

## is­Upper

### Description
Checks if a character is uppercase.

### Method
N/A (Function/Method Call)

### Endpoint
N/A

### Parameters
None

### Request Example
None

### Response
None

## is­Valid

### Description
Checks if a string position or slice position is valid.

### Method
N/A (Function/Method Call)

### Endpoint
N/A

### Parameters
None

### Request Example
None

### Response
None

## is­Valid­Char

### Description
Checks if a natural number or UInt32 is a valid character code.

### Method
N/A (Function/Method Call)

### Endpoint
N/A

### Parameters
None

### Request Example
None

### Response
None

## is­Valid­Char­Nat

### Description
Checks if a character is a valid character represented as a natural number.

### Method
N/A (Function/Method Call)

### Endpoint
N/A

### Parameters
None

### Request Example
None

### Response
None

## is­Valid­For­Slice

### Description
Checks if a string position or slice position is valid for slicing.

### Method
N/A (Function/Method Call)

### Endpoint
N/A

### Parameters
None

### Request Example
None

### Response
None

## is­Valid­UTF8

### Description
Checks if a string is valid UTF-8.

### Method
N/A (Function/Method Call)

### Endpoint
N/A

### Parameters
None

### Request Example
None

### Response
None

## is­Whitespace

### Description
Checks if a character is whitespace.

### Method
N/A (Function/Method Call)

### Endpoint
N/A

### Parameters
None

### Request Example
None

### Response
None

## is­Windows

### Description
Checks if the current platform is Windows.

### Method
N/A (Function/Method Call)

### Endpoint
N/A

### Parameters
None

### Request Example
None

### Response
None

## is­eqv

### Description
Checks for equivalence using the Setoid class.

### Method
N/A (Function/Method Call)

### Endpoint
N/A

### Parameters
None

### Request Example
None

### Response
None

## it

### Description
Represents an element in a termination measure or structure field.

### Method
N/A (Function/Method Call)

### Endpoint
N/A

### Parameters
None

### Request Example
None

### Response
None

## iter

### Description
Iterates over the elements of a collection (Array, List, HashMap, etc.).

### Method
N/A (Function/Method Call)

### Endpoint
N/A

### Parameters
None

### Request Example
None

### Response
None

## iter­From­Idx

### Description
Iterates over an array starting from a specific index.

### Method
N/A (Function/Method Call)

### Endpoint
N/A

### Parameters
None

### Request Example
None

### Response
None

## iter­From­Idx­M

### Description
Monadically iterates over an array starting from a specific index.

### Method
N/A (Function/Method Call)

### Endpoint
N/A

### Parameters
None

### Request Example
None

### Response
None

## iter­M

### Description
Monadically iterates over a collection (Array, List).

### Method
N/A (Function/Method Call)

### Endpoint
N/A

### Parameters
None

### Request Example
None

### Response
None

## iterate

### Description
Applies a function repeatedly to generate a sequence.

### Method
N/A (Function/Method Call)

### Endpoint
N/A

### Parameters
None

### Request Example
None

### Response
None

## iunfoldr

### Description
Unfolds a BitVec into a list using a function.

### Method
N/A (Function/Method Call)

### Endpoint
N/A

### Parameters
None

### Request Example
None

### Response
None

## iunfoldr_replace

### Description
Unfolds and replaces elements in a BitVec.

### Method
N/A (Function/Method Call)

### Endpoint
N/A

### Parameters
None

### Request Example
None

### Response
None
```

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

### Importing Module with Public Definition

Source: https://lean-lang.org/doc/reference/latest/Source-Files-and-Modules

Demonstrates importing a module where 'greeting' has been made public. The 'greetTwice' function can now successfully call 'greeting' because it is accessible.

```Lean
module import Greet.Create def greetTwice (name1 name2 : String) : String := greeting name1 ++ "\n" ++ greeting name2
```

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

### K Functions

Source: https://lean-lang.org/doc/reference/latest/the-index

Functions starting with the letter 'K'.

```APIDOC
## key­At­Idx!

### Description
Retrieves the key at a specific index in a TreeMap, raising an error if the index is out of bounds.

### Method
N/A (Function/Method Call)

### Endpoint
N/A

### Parameters
None

### Request Example
None

### Response
None

## key­At­Idx

### Description
Retrieves the key at a specific index in a TreeMap.

### Method
N/A (Function/Method Call)

### Endpoint
N/A

### Parameters
None

### Request Example
None

### Response
None

## key­At­Idx?

### Description
Safely retrieves the key at a specific index in a TreeMap, returning None if the index is out of bounds.

### Method
N/A (Function/Method Call)

### Endpoint
N/A

### Parameters
None

### Request Example
None

### Response
None

## key­At­Idx­D

### Description
Retrieves the key-value pair at a specific index in a TreeMap.

### Method
N/A (Function/Method Call)

### Endpoint
N/A

### Parameters
None

### Request Example
None

### Response
None

## keys

### Description
Returns an iterator over the keys of a map (DHashMap, DTreeMap, HashMap, TreeMap).

### Method
N/A (Function/Method Call)

### Endpoint
N/A

### Parameters
None

### Request Example
None

### Response
None

## keys­Array

### Description
Returns an array of keys from a map (DHashMap, DTreeMap, HashMap, TreeMap).

### Method
N/A (Function/Method Call)

### Endpoint
N/A

### Parameters
None

### Request Example
None

### Response
None

## keys­Iter

### Description
Returns an iterator over the keys of a map (DHashMap, DTreeMap, HashMap, TreeMap).

### Method
N/A (Function/Method Call)

### Endpoint
N/A

### Parameters
None

### Request Example
None

### Response
None

## kill

### Description
Sends a kill signal to a child process.

### Method
N/A (Function/Method Call)

### Endpoint
N/A

### Parameters
None

### Request Example
None

### Response
None

## kleisli­Left

### Description
Creates a Kleisli composition from the left.

### Method
N/A (Function/Method Call)

### Endpoint
N/A

### Parameters
None

### Request Example
None

### Response
None

## kleisli­Right

### Description
Creates a Kleisli composition from the right.

### Method
N/A (Function/Method Call)

### Endpoint
N/A

### Parameters
None

### Request Example
None

### Response
None
```

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

### General #guard_msgs Configuration

Source: https://lean-lang.org/doc/reference/latest/Interacting-with-Lean

Demonstrates the general syntax for `#guard_msgs` with a comma-separated list of configuration clauses, including a wildcard for checking all messages.

```lean
#guard_msgs (configElt,*) in cmd

```

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

### J Functions

Source: https://lean-lang.org/doc/reference/latest/the-index

Functions starting with the letter 'J'.

```APIDOC
## join

### Description
Joins elements of an Option, Format, or String, or path components.

### Method
N/A (Function/Method Call)

### Endpoint
N/A

### Parameters
None

### Request Example
None

### Response
None

## join­Sep

### Description
Joins elements of a Format with a separator.

### Method
N/A (Function/Method Call)

### Endpoint
N/A

### Parameters
None

### Request Example
None

### Response
None

## join­Suffix

### Description
Joins elements of a Format with a suffix.

### Method
N/A (Function/Method Call)

### Endpoint
N/A

### Parameters
None

### Request Example
None

### Response
None
```

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

### Define an initialize block with return type

Source: https://lean-lang.org/doc/reference/latest/Elaboration-and-Compilation

Use this syntax when initialization needs to return a value, such as an environment extension.

```lean
command ::= ...
    | 
declModifiers is the collection of modifiers on a declaration:




  * a doc comment /-- ... -/


  * a list of attributes @[attr1, attr2]


  * a visibility specifier, private or public


  * protected


  * noncomputable


  * unsafe


  * partial or nonrec




All modifiers are optional, and have to come in the listed order.


nestedDeclModifiers is the same as declModifiers, but attributes are printed
on the same line as the declaration. It is used for declarations nested inside other syntax,
such as inductive constructors, structure projections, and let rec / where definitions. 


initialize ident : term ←
        doSeqItem*
```

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

### Opening Entire Namespaces

Source: https://lean-lang.org/doc/reference/latest/Namespaces-and-Sections

Demonstrates opening multiple namespaces sequentially. Each namespace is considered relative to the currently open ones, allowing for nested scope resolution.

```lean
namespace A -- _root_.A
def a1 := 0
namespace B -- _root_.A.B
def a2 := 0
namespace C -- _root_.A.B.C
def a3 := 0
end C
end B
end A

namespace B -- _root_.B
def a4 := 0
namespace C -- _root_.B.C
def a5 := 0
end C
end B

namespace C -- _root_.C
def a6 := 0
end C
```

```lean
section open A B C example := [a1, a2, a3, a4, a5, a6] end
```

```lean
section open A.B C example := [
  a1, a2, a3, a4, a5, a6
] end
```

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

### Bind and Bind.mk

Source: https://lean-lang.org/doc/reference/latest/the-index

Documentation for the Bind type and its instance constructor.

```APIDOC
## Bind and Bind.mk

### Description
Documentation for the Bind type and its instance constructor.

### Method
N/A

### Endpoint
N/A

### Parameters
N/A

### Request Example
N/A

### Response
#### Success Response (200)
N/A

#### Response Example
N/A
```

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

### Iterator Operations

Source: https://lean-lang.org/doc/reference/latest/the-index

Operations for iterators, including getting the current element.

```APIDOC
## Iterator Operations

Operations for iterators.

### ByteArray.Iterator.curr'

### String.Legacy.Iterator.curr'

### ByteArray.Iterator.curr

### String.Legacy.Iterator.curr

```

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

### Evaluate NatOrInt.nat 5 in Lean

Source: https://lean-lang.org/doc/reference/latest/Interacting-with-Lean

Demonstrates the evaluation of `NatOrInt.nat 5` using `IO.println` and the `repr` function.

```lean
N.NatOrInt.nat 5
```

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

### Define a function in Lean

Source: https://lean-lang.org/doc/reference/latest/Interacting-with-Lean

A simple function definition used for evaluation examples.

```lean
module public section def isEven (n : Nat) : Bool := n % 2 = 0 
```

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

### Define a basic Lean function

Source: https://lean-lang.org/doc/reference/latest/Introduction

A simple example of a function definition in Lean.

```lean
def hello : IO Unit := IO.println "Hello, world!" 
```

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

### Lean Plain Import Syntax

Source: https://lean-lang.org/doc/reference/latest/Source-Files-and-Modules

Illustrates the basic syntax for importing a Lean file using a plain 'import' statement followed by an identifier.

```lean
import ::=
    | import ident
```

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

### Demonstrate ReprAtom with ABC Type

Source: https://lean-lang.org/doc/reference/latest/Interacting-with-Lean

Shows how ReprAtom influences list formatting for custom types.

```lean
inductive ABC where | a | b | c deriving Repr 
```

```lean
def abc : List ABC := [.a, .b, .c] def abcs : List ABC := abc ++ abc ++ abc 
```

```lean
def ABC.toNat : ABC → Nat | .a => 0 | .b => 1 | .c => 2 
```

```lean
instance : ReprAtom ABC := ⟨⟩ 
```

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

### Define an inductive predicate

Source: https://lean-lang.org/doc/reference/latest/Introduction

Example of defining even numbers using an inductive predicate.

```lean
inductive Even : Nat → Prop where | zero : Even 0 | plusTwo : Even n → Even (n + 2) 
```

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

### Open Namespace and Prove Theorem in Lean

Source: https://lean-lang.org/doc/reference/latest/Namespaces-and-Sections

Opens the Combinator.Calculus namespace for the entire section and proves a theorem using the imported combinators. 'I', 'K', and 'S' are directly accessible.

```Lean
section
  -- open everything under `Combinator.Calculus`, *i.e.* `I`, `K` and `S`,
  -- until the section ends
  open Combinator.Calculus

  theorem SKx_eq_K : S K x = I := rfl
end
```

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

### Display parser error messages

Source: https://lean-lang.org/doc/reference/latest/Introduction

Example of a syntax error and its corresponding location indicator.

```lean
def f : Option Nat → Type  | some 0 => Unit  |unexpected token '=>'; expected term => Option (f t)  | none => Empty
```

```text
<example>:3:3-3:6: unexpected token '=>'; expected term
```

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

### Using proofs to solve metavariables

Source: https://lean-lang.org/doc/reference/latest/Source-Files-and-Modules

Shows a definition using a proof to solve a metavariable in a plain source file.

```lean
structure Half (n : Nat) where val : Nat ok : val + val = n abbrev two := Half.mk _ <| by⊢ ?m.3 + ?m.3 = ?m.5 show 2 + 2 = 4⊢ 2 + 2 = 4 rflAll goals completed! 🐙 
```

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

### Display compiler error messages

Source: https://lean-lang.org/doc/reference/latest/Introduction

Example of a type mismatch error message during compilation.

```text
Application type mismatch: The argument
  "two"
has type
  String
but is expected to have type
  Nat
in the application
  Nat.succ "two"
```

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

### Display compiler warnings

Source: https://lean-lang.org/doc/reference/latest/Introduction

Example of a warning message indicating the use of sorry in a declaration.

```text
declaration uses `sorry`
```

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

### Lean Pattern Matching Syntax

Source: https://lean-lang.org/doc/reference/latest/Definitions/Definitions

Demonstrates the syntax for pattern matching in Lean, including its desugaring to `Lean.Parser.Term.match`. Covers matching terms, alternatives, and the use of `generalizing` for dependent types.

```lean
command ::= ...
    | 
declModifiers is the collection of modifiers on a declaration:



  * a doc comment /-- ... -/


  * a list of attributes @[attr1, attr2]


  * a visibility specifier, private or public


  * protected


  * noncomputable


  * unsafe


  * partial or nonrec



All modifiers are optional, and have to come in the listed order.


nestedDeclModifiers is the same as declModifiers, but attributes are printed
on the same line as the declaration. It is used for declarations nested inside other syntax,
such as inductive constructors, structure projections, and let rec / where definitions.


declModifiers
      def 
declId matches foo or foo.{u,v}: an identifier possibly followed by a list of universe names 

declId 
optDeclSig matches the signature of a declaration with optional type: a list of binders and then possibly : type 

optDeclSig
        (| term => term)*
Termination hints are termination_by and decreasing_by, in that order.
```

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

### Warning for Unused Included Variable

Source: https://lean-lang.org/doc/reference/latest/Namespaces-and-Sections

Example of a warning generated when an included section variable is not used in a theorem.

```Lean
included section variable '[ToString α]' is not used in 'ex', consider excluding it
```

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

### Evaluate NatOrInt.int 5 in Lean

Source: https://lean-lang.org/doc/reference/latest/Interacting-with-Lean

Demonstrates the evaluation of `NatOrInt.int 5` using `IO.println` and the `repr` function.

```lean
N.NatOrInt.int 5
```

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

### Check `pal!` macro usage in Lean

Source: https://lean-lang.org/doc/reference/latest/Source-Files-and-Modules

Example of using the `pal!` macro with an array literal and concatenation.

```lean
#check pal! (#[1, 2, 3] ++ [6, 7, 8])
```

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

### Define builtin_initialize syntax

Source: https://lean-lang.org/doc/reference/latest/Elaboration-and-Compilation

Syntax definition for the builtin_initialize command using doSeqItem.

```Lean
builtin_initialize ident : term ←
        doSeqItem*
```

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

### Demonstrate contradiction with free theorem

Source: https://lean-lang.org/doc/reference/latest/Axioms

A proof script showing how the non-parametric function contradicts the free theorem axiom.

```lean
theorem unit_not_nat : Unit ≠ Nat := by⊢ Unit ≠ Nat intro eqeq:Unit = Nat⊢ False have ⟨allEq⟩ := eq ▸ (inferInstance : Subsingleton Unit)eq:Unit = NatallEq:∀ (a b : Nat), a = b⊢ False specialize allEq 0 1eq:Unit = NatallEq:0 = 1⊢ False contradictionAll goals completed! 🐙 example : False := by⊢ False have := List.free_theorem nonParametric (fun () => 42)this:(nonParametric ∘ List.map fun x => 42) = (List.map fun x => 42) ∘ nonParametric⊢ False unfold nonParametric at thisthis:((fun xs => if Nat = Nat then [] else xs) ∘ List.map fun x => 42) = (List.map fun x => 42) ∘ fun xs => if Unit = Nat then [] else xs⊢ False simp [unit_not_nat] at thisthis:((fun xs => []) ∘ List.map fun x => 42) = (List.map fun x => 42) ∘ fun xs => xs⊢ False have := congrFun this [()]this✝:((fun xs => []) ∘ List.map fun x => 42) = (List.map fun x => 42) ∘ fun xs => xsthis:((fun xs => []) ∘ List.map fun x => 42) [()] = ((List.map fun x => 42) ∘ fun xs => xs) [()]⊢ False contradictionAll goals completed! 🐙 
```

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

### Define thirdOfFive function

Source: https://lean-lang.org/doc/reference/latest/Elaboration-and-Compilation

Example of a function definition using pattern matching that generates equational lemmas.

```lean
def thirdOfFive : List α → Option α | [_, _, x, _, _] => some x | _ => none 
```

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

### File System and IO Operations

Source: https://lean-lang.org/doc/reference/latest/the-index

Documentation for file system and Input/Output operations in Lean, including directory and file creation.

```APIDOC
## File System and IO Operations

Documentation for file system and Input/Output operations in Lean.

### IO.FS.create_Dir

### IO.FS.create_Dir_All

### IO.FS.create_Temp_Dir

### IO.FS.create_Temp_File

### IO.current_Dir

```

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

### #guard_msgs with Error Filter

Source: https://lean-lang.org/doc/reference/latest/Interacting-with-Lean

Captures only error messages generated by a command. This example checks for an error when 'sorry' is used.

```lean
#guard_msgs(error) in
example : α := sorry
```

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

### Filter Errors with #guard_msgs

Source: https://lean-lang.org/doc/reference/latest/Interacting-with-Lean

Selects only error messages from the `example` command. Warnings are not captured, as demonstrated by the `sorry` declaration.

```lean
#guard_msgs(error) in
example : α := sorry

```

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

### Lean 4 Environment Serialization and Compilation

Source: https://lean-lang.org/doc/reference/latest/Elaboration-and-Compilation

Overview of the .olean, .ilean file formats and the C compilation process.

```APIDOC
## Environment Serialization and Compilation

### .olean Files
- **Purpose**: Serialized global environment data including types and definitions.
- **Characteristics**: Directly memory-mapped; validated by the kernel or the `lean4checker` tool.

### .ilean Files
- **Purpose**: Index file used by the language server for interactive development.
- **Content**: Contains source positions and metadata; implementation details are subject to change.

### Compilation Process
- **Mechanism**: Translates intermediate representation to C code.
- **Execution**: Compiled to native code via a bundled C compiler.
- **Options**: If `precompileModules` is enabled, native code is dynamically loaded; otherwise, an interpreter is used.
```

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

### Basic section command syntax in Lean

Source: https://lean-lang.org/doc/reference/latest/Namespaces-and-Sections

Shows the basic syntax for the `section` command, which can optionally be followed by an identifier to name the section.

```lean
command ::= ...
    | section section ident?

```

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

### Filter Warnings with #guard_msgs

Source: https://lean-lang.org/doc/reference/latest/Interacting-with-Lean

Selects only warning messages from the `example` command and checks them against the docstring. Other message types are ignored.

```lean
/--
warning: declaration uses 'sorry'
-/ 
#guard_msgs(warning) in
example : α := sorry

```