# HigherOrder attribute #

This file defines the `@[higher_order]`

attribute that applies to lemmas of the shape
`∀ x, f (g x) = h x`

. It derives an auxiliary lemma of the form `f ∘ g = h`

for reasoning about
higher-order functions.

## Equations

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

## Instances For

`mkComp v e`

checks whether `e`

is a sequence of nested applications `f (g (h v))`

, and if so,
returns the expression `f ∘ g ∘ h`

. If `e = v`

it returns `id`

.

## Equations

- One or more equations did not get rendered due to their size.
- Tactic.mkComp v x = do guard (x.equal v = true) let t ← Lean.Meta.inferType x Lean.Meta.mkAppOptM `id #[some t]

## Instances For

From a lemma of the shape `∀ x, f (g x) = h x`

derive an auxiliary lemma of the form `f ∘ g = h`

for reasoning about higher-order functions.

A user attribute that applies to lemmas of the shape `∀ x, f (g x) = h x`

.
It derives an auxiliary lemma of the form `f ∘ g = h`

for reasoning about higher-order functions.

## Equations

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

## Instances For

The `higher_order`

attribute. From a lemma of the shape `∀ x, f (g x) = h x`

derive an
auxiliary lemma of the form `f ∘ g = h`

for reasoning about higher-order functions.

Syntax: `[higher_order]`

or `[higher_order name]`

where the given name is used for the
generated theorem.