Commit 2023-01-17 11:01 f25f56f6

feat: interval_cases tactic (#1155) Implements the interval_cases tactic from mathlib. This is a from scratch implementation, which should be a lot faster and give better goals than the original. I also tried to make a reasonable MetaM version of the tactic. The original tactic was very generic and used typeclass inference to find most of the structure on the type. The new one is still somewhat type-generic but relies on meta-instances which implement the required functionality for supported types. Currently only Nat and Int are supported; PNat is more difficult because norm_num doesn't work on it.