New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

remove false remarks about structures that only held in Lean 3 #121

Merged

PatrickMassot merged 1 commit into avigad:master from eric-wieser:structure-eta

Aug 30, 2023

Contributor

eric-wieser commented Aug 30, 2023 •

edited

Loading

cases is no longer needed when writing definitions in terms of pattern matches, though mathlib still prefers to avoid doing so.

I think the mathlib community are still hesitant to use this feature, so I've added a hand-wave about more awkward goal views.

If leanprover/lean4#2042 is addressed, there will be more interesting things to say about this alternate spelling, but for now there isn't really.


          remove false remarks that only held in Lean 3

d0c3b4e

PatrickMassot merged commit 9c5e08a into avigad:master

1 check passed

Collaborator

PatrickMassot commented Aug 30, 2023

Thanks. I knew something became wrong but forgot to investigate.

avigad mentioned this pull request

Explain structural eta reduction #124

Open

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment