Documentation

Mathlib.Tactic.HigherOrder

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.

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

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.

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.