Commit 2023-03-30 13:54 ac1e75f5
View on Github →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
cases f₁ using WithBot.recBotCoe with
| h₁ => …
| h₂ f₁ => …
we would prefer to be able to write
cases f₁ using WithBot.recBotCoe with
| bot => …
| coe f₁ => …
and rather than
induction s using cons_induction with
| h₁ => …
| @h₂ c s hc ih => …
we would prefer
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 _ _ _.