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.
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
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.