Commit 2023-02-09 13:57 bac7310c

feat: port Tactic.Slice (#2109) Ports the slice and its descendants. The new syntax is slice_lhs a b => tac. Beyond a new Slice.lean and a test file, there are changes to Mathlib.Tactic.Core adding iteration tactics and replacing a MonadExceptOf instance assumption by a MonadExcept instance for these tactics.