Documentation
Lean
.
Meta
.
Sym
.
DSimp
.
Let
Search
return to top
source
Imports
Lean.Meta.Sym.AbstractS
Lean.Meta.Sym.InstantiateS
Lean.Meta.Sym.DSimp.DSimpM
Imported by
Lean
.
Meta
.
Sym
.
DSimp
.
dsimpLet
source
def
Lean
.
Meta
.
Sym
.
DSimp
.
dsimpLet
:
DSimproc
Definitionally simplifies a
let
/
have
expression.
Instances For