Def Lean.Parser.Term.letIdLhs'

Modification history

2022-03-22 05:59
Mathlib/Tactic/Have.lean
fix: `let` should be using `haveIdLhs` (#246)
Deleted Lean.Parser.Term.letIdLhs'View on Github →
2022-03-22 05:33
Mathlib/Tactic/Have.lean
feat: extended `have` and `let` tactics (#232)
Added Lean.Parser.Term.letIdLhs'View on Github →