← Mathematical handbook

def Lean.Meta.Sym.DSimp.dsimpLet : DSimproc

Definitionally simplifies a let/have expression.

Equations

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