Commit 2023-01-17 11:01 f25f56f6
View on Github →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.