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

• Lean.Meta.Sym.DSimp.dsimpLambda e = Lean.Meta.Sym.DSimp.dsimpLambda.go✝ e #[] false