Commit 2022-03-14 18:42 72341a8e

View on Github →

feat : simpa tactic (#224)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Mathport/Syntax.lean

Modified Mathlib/Tactic/Core.lean

added def Lean.Parser.Tactic.getSimpArgs

added def Lean.Parser.Tactic.getUsingArg

added def Lean.Parser.Tactic.getWithArgs

Created Mathlib/Tactic/Simpa.lean

Created test/Simpa.lean

added def foo