This module contains a pass for inlining lambda abstractions that are bound by bindings of let-expressions into the in-expressions.

The purpose of this pass is to avoid the generation of share operators for lambda abstractions. Since lambda abstractions are not evaluated by any evaluation strategy until they are invoked, the inlining does not change the semantics of the program. The inlining helps Coq's termination checker sometimes if the lambda abstraction contains recursive calls.

Example

Expressions of the form

let { f = \x -> e } in g f

are replaced by expressions of the form

g (\x -> e)

Specification

Preconditions

All functions are fully applied (i.e., fully η-converted).

Translation

For every let-expression

let {x₁ = e₁ ; … ; xₙ = eₙ} in e

all bindings xᵢ = eᵢ whose right-hand side eᵢ is a lambda abstraction, are removed and all occurences of xᵢ in e are replaced by eᵢ.

Postconditions

There are no let-bindings whose right-hand side is a lambda-abstraction.