Commit 2022-02-07 12:43 09097f67
View on Github →feat: cases' and induction' tactics (#183)
This adds a lean 3 compatible syntax for cases and induction: cases' x with a b c d, induction' x with a b ih_b c ih_c
feat: cases' and induction' tactics (#183)
This adds a lean 3 compatible syntax for cases and induction: cases' x with a b c d, induction' x with a b ih_b c ih_c