Commit 2022-03-22 05:33 6f2b6764

View on Github →

feat: extended have and let tactics (#232)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/Array/Defs.lean

added def Array.flatten

Modified Mathlib/Mathport/Syntax.lean

Created Mathlib/Tactic/Have.lean

added def Lean.Parser.Term.haveIdLhs'

added def Lean.Parser.Term.letIdLhs'

added def Mathlib.Tactic.haveLetCore

Created test/Have.lean