Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
refactor: hypothesis naming in custom recursors (#1658)
I have renamed hypotheses in `WithBot.recBotCoe`, `WithTop.recTopCoe` and `Finset.cons_induction` on the basis that rather than ```lean cases f₁ using WithBot.recBotCoe with | h₁ => … | h₂ f₁ => … ``` we would prefer to be able to write ```lean cases f₁ using WithBot.recBotCoe with | bot => … | coe f₁ => … ``` and rather than ```lean induction s using cons_induction with | h₁ => … | @h₂ c s hc ih => … ``` we would prefer ```lean induction s using cons_induction with | empty => … | @COns c t hc ih => … ```` I also tidied up some of inf' stuff in Finset.Lattice by using named arguments to specify the dual type instead of `@`s and `_ _ _`.
- Loading branch information
1 parent
d38f441
commit ac1e75f
Showing
4 changed files
with
70 additions
and
78 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters