Documentation
Lean
.
Elab
.
Tactic
.
Conv
.
Lets
Search
return to top
source
Imports
Lean.Elab.Tactic.Lets
Lean.Elab.Tactic.Conv.Basic
Imported by
Conv tactics to manipulate
let
expressions
#
extract_lets
#
lift_lets
#