## 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 (Array.size elems - 1) (Array.back elems)

## Instances For

Return `some`

if succeeded expanding `·`

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

.
Examples:

`· + 1`

=>`fun _a_1 => _a_1 + 1`

`f · · b`

=>`fun _a_1 _a_2 => f _a_1 _a_2 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 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? true true pure (Lean.Meta.DiscrTree.mkNoindexAnnotation e)