def PQXDHLean.Tactics.matchProbOutput?
  (eLean.Expr : Lean.ExprLean.Expr : TypeLean expressions. This data structure is used in the kernel and
elaborator. However, expressions sent to the kernel should not
contain metavariables.

Remark: we use the `E` suffix (short for `Expr`) to avoid collision with keywords.
We considered using «...», but it is too inconvenient to use.
) :
  OptionOption.{u} (α : Type u) : Type uOptional values, which are either `some` around a value from the underlying type or `none`.

`Option` can represent nullable types or computations that might fail. In the codomain of a function
type, it can also represent partiality.
 (Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`.Lean.ExprLean.Expr : TypeLean expressions. This data structure is used in the kernel and
elaborator. However, expressions sent to the kernel should not
contain metavariables.

Remark: we use the `E` suffix (short for `Expr`) to avoid collision with keywords.
We considered using «...», but it is too inconvenient to use.
 ×Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`. Lean.ExprLean.Expr : TypeLean expressions. This data structure is used in the kernel and
elaborator. However, expressions sent to the kernel should not
contain metavariables.

Remark: we use the `E` suffix (short for `Expr`) to avoid collision with keywords.
We considered using «...», but it is too inconvenient to use.
)Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`.

def PQXDHLean.Tactics.matchProbEvent?
  (eLean.Expr : Lean.ExprLean.Expr : TypeLean expressions. This data structure is used in the kernel and
elaborator. However, expressions sent to the kernel should not
contain metavariables.

Remark: we use the `E` suffix (short for `Expr`) to avoid collision with keywords.
We considered using «...», but it is too inconvenient to use.
) :
  OptionOption.{u} (α : Type u) : Type uOptional values, which are either `some` around a value from the underlying type or `none`.

`Option` can represent nullable types or computations that might fail. In the codomain of a function
type, it can also represent partiality.
 (Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`.Lean.ExprLean.Expr : TypeLean expressions. This data structure is used in the kernel and
elaborator. However, expressions sent to the kernel should not
contain metavariables.

Remark: we use the `E` suffix (short for `Expr`) to avoid collision with keywords.
We considered using «...», but it is too inconvenient to use.
 ×Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`. Lean.ExprLean.Expr : TypeLean expressions. This data structure is used in the kernel and
elaborator. However, expressions sent to the kernel should not
contain metavariables.

Remark: we use the `E` suffix (short for `Expr`) to avoid collision with keywords.
We considered using «...», but it is too inconvenient to use.
)Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`.

def PQXDHLean.Tactics.parseProbEqSides
  (targetLean.Expr : Lean.ExprLean.Expr : TypeLean expressions. This data structure is used in the kernel and
elaborator. However, expressions sent to the kernel should not
contain metavariables.

Remark: we use the `E` suffix (short for `Expr`) to avoid collision with keywords.
We considered using «...», but it is too inconvenient to use.
) :
  Lean.MetaMLean.Meta.MetaM (α : Type) : TypeThe `MetaM` monad is a core component of Lean's metaprogramming framework, facilitating the
construction and manipulation of expressions (`Lean.Expr`) within Lean.

It builds on top of `CoreM` and additionally provides:
- A `LocalContext` for managing free variables.
- A `MetavarContext` for managing metavariables.
- A `Cache` for caching results of the key `MetaM` operations.

The key operations provided by `MetaM` are:
- `inferType`, which attempts to automatically infer the type of a given expression.
- `whnf`, which reduces an expression to the point where the outermost part is no longer reducible
  but the inside may still contain unreduced expression.
- `isDefEq`, which determines whether two expressions are definitionally equal, possibly assigning
  meta variables in the process.
- `forallTelescope` and `lambdaTelescope`, which make it possible to automatically move into
  (nested) binders while updating the local context.

The following is a small example that demonstrates how to obtain and manipulate the type of a
`Fin` expression:
```
public import Lean

open Lean Meta

def getFinBound (e : Expr) : MetaM (Option Expr) := do
  let type ← whnf (← inferType e)
  let_expr Fin bound := type | return none
  return bound

def a : Fin 100 := 42

run_meta
  match ← getFinBound (.const ``a []) with
  | some limit => IO.println (← ppExpr limit)
  | none => IO.println "no limit found"
```

    (OptionOption.{u} (α : Type u) : Type uOptional values, which are either `some` around a value from the underlying type or `none`.

`Option` can represent nullable types or computations that might fail. In the codomain of a function
type, it can also represent partiality.

      (Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`.Lean.ExprLean.Expr : TypeLean expressions. This data structure is used in the kernel and
elaborator. However, expressions sent to the kernel should not
contain metavariables.

Remark: we use the `E` suffix (short for `Expr`) to avoid collision with keywords.
We considered using «...», but it is too inconvenient to use.
 ×Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`. Lean.ExprLean.Expr : TypeLean expressions. This data structure is used in the kernel and
elaborator. However, expressions sent to the kernel should not
contain metavariables.

Remark: we use the `E` suffix (short for `Expr`) to avoid collision with keywords.
We considered using «...», but it is too inconvenient to use.
 ×Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`. Lean.ExprLean.Expr : TypeLean expressions. This data structure is used in the kernel and
elaborator. However, expressions sent to the kernel should not
contain metavariables.

Remark: we use the `E` suffix (short for `Expr`) to avoid collision with keywords.
We considered using «...», but it is too inconvenient to use.
)Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`.)

def PQXDHLean.Tactics.computePermutation
  (pairsArray (ℕ × ℕ) : ArrayArray.{u} (α : Type u) : Type u`Array α` is the type of [dynamic arrays](https://en.wikipedia.org/wiki/Dynamic_array) with elements
from `α`. This type has special support in the runtime.

Arrays perform best when unshared. As long as there is never more than one reference to an array,
all updates will be performed _destructively_. This results in performance comparable to mutable
arrays in imperative programming languages.

An array has a size and a capacity. The size is the number of elements present in the array, while
the capacity is the amount of memory currently allocated for elements. The size is accessible via
`Array.size`, but the capacity is not observable from Lean code. `Array.emptyWithCapacity n` creates
an array which is equal to `#[]`, but internally allocates an array of capacity `n`. When the size
exceeds the capacity, allocation is required to grow the array.

From the point of view of proofs, `Array α` is just a wrapper around `List α`.
 (Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`.ℕNat : TypeThe natural numbers, starting at zero.

This type is special-cased by both the kernel and the compiler, and overridden with an efficient
implementation. Both use a fast arbitrary-precision arithmetic library (usually
[GMP](https://gmplib.org/)); at runtime, `Nat` values that are sufficiently small are unboxed.
 ×Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`. ℕNat : TypeThe natural numbers, starting at zero.

This type is special-cased by both the kernel and the compiler, and overridden with an efficient
implementation. Both use a fast arbitrary-precision arithmetic library (usually
[GMP](https://gmplib.org/)); at runtime, `Nat` values that are sufficiently small are unboxed.
)Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)The product type, usually written `α × β`. Product types are also called pair or tuple types.
Elements of this type are pairs in which the first element is an `α` and the second element is a
`β`.

Products nest to the right, so `(x, y, z) : α × β × γ` is equivalent to `(x, (y, z)) : α × (β × γ)`.


Conventions for notations in identifiers:

 * The recommended spelling of `×` in identifiers is `Prod`.) (nLℕ nRℕ : ℕNat : TypeThe natural numbers, starting at zero.

This type is special-cased by both the kernel and the compiler, and overridden with an efficient
implementation. Both use a fast arbitrary-precision arithmetic library (usually
[GMP](https://gmplib.org/)); at runtime, `Nat` values that are sufficiently small are unboxed.
) :
  Lean.MetaMLean.Meta.MetaM (α : Type) : TypeThe `MetaM` monad is a core component of Lean's metaprogramming framework, facilitating the
construction and manipulation of expressions (`Lean.Expr`) within Lean.

It builds on top of `CoreM` and additionally provides:
- A `LocalContext` for managing free variables.
- A `MetavarContext` for managing metavariables.
- A `Cache` for caching results of the key `MetaM` operations.

The key operations provided by `MetaM` are:
- `inferType`, which attempts to automatically infer the type of a given expression.
- `whnf`, which reduces an expression to the point where the outermost part is no longer reducible
  but the inside may still contain unreduced expression.
- `isDefEq`, which determines whether two expressions are definitionally equal, possibly assigning
  meta variables in the process.
- `forallTelescope` and `lambdaTelescope`, which make it possible to automatically move into
  (nested) binders while updating the local context.

The following is a small example that demonstrates how to obtain and manipulate the type of a
`Fin` expression:
```
public import Lean

open Lean Meta

def getFinBound (e : Expr) : MetaM (Option Expr) := do
  let type ← whnf (← inferType e)
  let_expr Fin bound := type | return none
  return bound

def a : Fin 100 := 42

run_meta
  match ← getFinBound (.const ``a []) with
  | some limit => IO.println (← ppExpr limit)
  | none => IO.println "no limit found"
```
 (ArrayArray.{u} (α : Type u) : Type u`Array α` is the type of [dynamic arrays](https://en.wikipedia.org/wiki/Dynamic_array) with elements
from `α`. This type has special support in the runtime.

Arrays perform best when unshared. As long as there is never more than one reference to an array,
all updates will be performed _destructively_. This results in performance comparable to mutable
arrays in imperative programming languages.

An array has a size and a capacity. The size is the number of elements present in the array, while
the capacity is the amount of memory currently allocated for elements. The size is accessible via
`Array.size`, but the capacity is not observable from Lean code. `Array.emptyWithCapacity n` creates
an array which is equal to `#[]`, but internally allocates an array of capacity `n`. When the size
exceeds the capacity, allocation is required to grow the array.

From the point of view of proofs, `Array α` is just a wrapper around `List α`.
 ℕNat : TypeThe natural numbers, starting at zero.

This type is special-cased by both the kernel and the compiler, and overridden with an efficient
implementation. Both use a fast arbitrary-precision arithmetic library (usually
[GMP](https://gmplib.org/)); at runtime, `Nat` values that are sufficiently small are unboxed.
)

def PQXDHLean.Tactics.bubbleSortSwaps
  (targetIndicesArray ℕ : ArrayArray.{u} (α : Type u) : Type u`Array α` is the type of [dynamic arrays](https://en.wikipedia.org/wiki/Dynamic_array) with elements
from `α`. This type has special support in the runtime.

Arrays perform best when unshared. As long as there is never more than one reference to an array,
all updates will be performed _destructively_. This results in performance comparable to mutable
arrays in imperative programming languages.

An array has a size and a capacity. The size is the number of elements present in the array, while
the capacity is the amount of memory currently allocated for elements. The size is accessible via
`Array.size`, but the capacity is not observable from Lean code. `Array.emptyWithCapacity n` creates
an array which is equal to `#[]`, but internally allocates an array of capacity `n`. When the size
exceeds the capacity, allocation is required to grow the array.

From the point of view of proofs, `Array α` is just a wrapper around `List α`.
 ℕNat : TypeThe natural numbers, starting at zero.

This type is special-cased by both the kernel and the compiler, and overridden with an efficient
implementation. Both use a fast arbitrary-precision arithmetic library (usually
[GMP](https://gmplib.org/)); at runtime, `Nat` values that are sufficiently small are unboxed.
) : ArrayArray.{u} (α : Type u) : Type u`Array α` is the type of [dynamic arrays](https://en.wikipedia.org/wiki/Dynamic_array) with elements
from `α`. This type has special support in the runtime.

Arrays perform best when unshared. As long as there is never more than one reference to an array,
all updates will be performed _destructively_. This results in performance comparable to mutable
arrays in imperative programming languages.

An array has a size and a capacity. The size is the number of elements present in the array, while
the capacity is the amount of memory currently allocated for elements. The size is accessible via
`Array.size`, but the capacity is not observable from Lean code. `Array.emptyWithCapacity n` creates
an array which is equal to `#[]`, but internally allocates an array of capacity `n`. When the size
exceeds the capacity, allocation is required to grow the array.

From the point of view of proofs, `Array α` is just a wrapper around `List α`.
 ℕNat : TypeThe natural numbers, starting at zero.

This type is special-cased by both the kernel and the compiler, and overridden with an efficient
implementation. Both use a fast arbitrary-precision arithmetic library (usually
[GMP](https://gmplib.org/)); at runtime, `Nat` values that are sufficiently small are unboxed.

def PQXDHLean.Tactics.mkSwapProofTerm
  (depthℕ : ℕNat : TypeThe natural numbers, starting at zero.

This type is special-cased by both the kernel and the compiler, and overridden with an efficient
implementation. Both use a fast arbitrary-precision arithmetic library (usually
[GMP](https://gmplib.org/)); at runtime, `Nat` values that are sufficiently small are unboxed.
) :
  Lean.Elab.Tactic.TacticMLean.Elab.Tactic.TacticM (α : Type) : TypeThe tactic monad, which extends the term elaboration monad `TermElabM` with state that contains the
current goals (`Lean.Elab.Tactic.State`, accessible via `MonadStateOf`) and local information about
the current tactic's name and whether error recovery is enabled (`Lean.Elab.Tactic.Context`,
accessible via `MonadReaderOf`).

    (Lean.TSyntax (ks : Lean.SyntaxNodeKinds) : TypeTyped syntax, which tracks the potential kinds of the `Syntax` it contains.

While syntax quotations produce or expect `TSyntax` values of the correct kinds, this is not
otherwise enforced; it can easily be circumvented by direct use of the constructor.
Lean.TSyntaxLean.TSyntax (ks : Lean.SyntaxNodeKinds) : TypeTyped syntax, which tracks the potential kinds of the `Syntax` it contains.

While syntax quotations produce or expect `TSyntax` values of the correct kinds, this is not
otherwise enforced; it can easily be circumvented by direct use of the constructor.
 `term)Lean.TSyntax (ks : Lean.SyntaxNodeKinds) : TypeTyped syntax, which tracks the potential kinds of the `Syntax` it contains.

While syntax quotations produce or expect `TSyntax` values of the correct kinds, this is not
otherwise enforced; it can easily be circumvented by direct use of the constructor.

def PQXDHLean.Tactics.emitLhsSwap
  (depthℕ : ℕNat : TypeThe natural numbers, starting at zero.

This type is special-cased by both the kernel and the compiler, and overridden with an efficient
implementation. Both use a fast arbitrary-precision arithmetic library (usually
[GMP](https://gmplib.org/)); at runtime, `Nat` values that are sufficiently small are unboxed.
) :
  Lean.Elab.Tactic.TacticMLean.Elab.Tactic.TacticM (α : Type) : TypeThe tactic monad, which extends the term elaboration monad `TermElabM` with state that contains the
current goals (`Lean.Elab.Tactic.State`, accessible via `MonadStateOf`) and local information about
the current tactic's name and whether error recovery is enabled (`Lean.Elab.Tactic.Context`,
accessible via `MonadReaderOf`).
 UnitUnit : TypeThe canonical type with one element. This element is written `()`.

`Unit` has a number of uses:
* It can be used to model control flow that returns from a function call without providing other
  information.
* Monadic actions that return `Unit` have side effects without computing values.
* In polymorphic types, it can be used to indicate that no data is to be stored in a particular
  field.

def PQXDHLean.Tactics.emitInsertUnusedDraw
  (sampleExprLean.Expr zLean.Expr : Lean.ExprLean.Expr : TypeLean expressions. This data structure is used in the kernel and
elaborator. However, expressions sent to the kernel should not
contain metavariables.

Remark: we use the `E` suffix (short for `Expr`) to avoid collision with keywords.
We considered using «...», but it is too inconvenient to use.
) :
  Lean.Elab.Tactic.TacticMLean.Elab.Tactic.TacticM (α : Type) : TypeThe tactic monad, which extends the term elaboration monad `TermElabM` with state that contains the
current goals (`Lean.Elab.Tactic.State`, accessible via `MonadStateOf`) and local information about
the current tactic's name and whether error recovery is enabled (`Lean.Elab.Tactic.Context`,
accessible via `MonadReaderOf`).
 UnitUnit : TypeThe canonical type with one element. This element is written `()`.

`Unit` has a number of uses:
* It can be used to model control flow that returns from a function call without providing other
  information.
* Monadic actions that return `Unit` have side effects without computing values.
* In polymorphic types, it can be used to indicate that no data is to be stored in a particular
  field.