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.

def Lean.Parser.Attr.higherOrder : Lean.ParserDescr

Equations

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

def Tactic.mkComp (v : Lean.Expr) : Lean.Expr → Lean.MetaM Lean.Expr

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]

partial def Tactic.mkHigherOrderType (e : Lean.Expr) : Lean.MetaM Lean.Expr

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.

def Tactic.higherOrderGetParam (thm : Lean.Name) (stx : Lean.Syntax) : Lean.AttrM Lean.Name

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.

opaque Tactic.higherOrderAttr : Lean.ParametricAttribute Lean.Name

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.