Def Lean.Expr.letDepth

Modification history

2023-09-10 13:09

Mathlib/Lean/Expr/Basic.lean

refactor: re-home some meta code (#6921)

Modified Lean.Expr.letDepth View on Github →

2023-06-29 02:25

Mathlib/Tactic/ExtractLets.lean

feat: `extract_lets` tactic (#3897) …

Added Lean.Expr.letDepth View on Github →