lean4-htt

Author SHA1 Message Date

Author	SHA1	Message	Date
Kyle Miller	c4bfe25d18	feat: make `rcases` use the custom `Nat` eliminator (#3747 ) As a special case, makes the `rcases` machinery use `Nat.casesAuxOn` so that goal states see `0` and `n + 1` rather than `Nat.zero` and `Nat.succ n`. This is a followup to enabling custom eliminators for `cases` and `induction`. This doesn't use custom eliminators in general since `rcases` uses `Lean.MVarId.cases`, which is completely different from what `cases` and `induction` use.	2024-04-13 16:55:48 +00:00
Scott Morrison	755de48ff3	chore: upstream orphaned tests from Std (#3539 )	2024-02-29 04:12:52 +00:00

Kyle Miller

c4bfe25d18

feat: make rcases use the custom Nat eliminator (#3747 )

As a special case, makes the `rcases` machinery use `Nat.casesAuxOn` so
that goal states see `0` and `n + 1` rather than `Nat.zero` and
`Nat.succ n`. This is a followup to enabling custom eliminators for
`cases` and `induction`.

This doesn't use custom eliminators in general since `rcases` uses
`Lean.MVarId.cases`, which is completely different from what `cases` and
`induction` use.

2024-04-13 16:55:48 +00:00

Scott Morrison

755de48ff3

chore: upstream orphaned tests from Std (#3539 )

2024-02-29 04:12:52 +00:00

2 commits