## Equations

- One or more equations did not get rendered due to their size.

## Instances For

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

Return syntax `Prod.mk elems[0] (Prod.mk elems[1] ... (Prod.mk elems[elems.size - 2] elems[elems.size - 1])))`

## Equations

- Lean.Elab.Term.mkPairs elems = Lean.Elab.Term.mkPairs.loop elems (elems.size - 1) elems.back!

## Instances For

Return syntax `PProd.mk elems[0] (PProd.mk elems[1] ... (PProd.mk elems[elems.size - 2] elems[elems.size - 1])))`

## Equations

- Lean.Elab.Term.mkPPairs elems = Lean.Elab.Term.mkPPairs.loop elems (elems.size - 1) elems.back!

## Instances For

Return syntax `MProd.mk elems[0] (MProd.mk elems[1] ... (MProd.mk elems[elems.size - 2] elems[elems.size - 1])))`

## Equations

- Lean.Elab.Term.mkMPairs elems = Lean.Elab.Term.mkMPairs.loop elems (elems.size - 1) elems.back!

## Instances For

Return `some`

if succeeded expanding `·`

notation occurring in
the given syntax. Otherwise, return `none`

.
Examples:

`· + 1`

=>`fun x => x + 1`

`f · · b`

=>`fun x1 x2 => f x1 x2 b`

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

Auxiliary function for expanding the `·`

notation.
The extra state `Array Syntax`

contains the new binder names.
If `stx`

is a `·`

, we create a fresh identifier, store it in the
extra state, and return it. Otherwise, we just return `stx`

.

Helper method for elaborating terms such as `(.+.)`

where a constant name is expected.
This method is usually used to implement tactics that take function names as arguments
(e.g., `simp`

).

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

## Equations

- Lean.Elab.Term.elabNoindex stx expectedType? = do let e ← Lean.Elab.Term.elabTerm stx[1] expectedType? pure (Lean.Meta.DiscrTree.mkNoindexAnnotation e)

## Instances For

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

Elaborator for `by_elab`

.

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

## Equations

- One or more equations did not get rendered due to their size.