Documentation

Lean.Meta.Sym.DSimp.Lambda

← Mathematical handbook
source
def Lean.Meta.Sym.DSimp.dsimpLambda :
DSimproc

Definitionally simplifies a lambda expression.

Unlike Sym.Simp.simpLambda, it descends into the binder type as well as the body.

Equations
Instances For