Revise have syntax, once more
#479
Merged
Conversation
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
ChrisHughes24
pushed a commit
to ChrisHughes24/lean4
that referenced
this pull request
Dec 2, 2022
My first attempt to port a file to mathlib4. Please review my code style carefully -- I'm still not 100% sure about the rules yet. Notes: 1) The file uses `Function.surjective.forall` once, and this declaration is in Mathlib.Logic.Function.Basic. Conversely, importing that file gives us everything we need. As a result the imports in this file look totally unrelated to the corresponding imports in the mathlib3 file. 2) The proof of `mk.inj_iff` in mathlib3 was `by simp` but this failed in mathlib4 so I knocked up a longer proof (lines 56-57). Should I worry about this? In Lean 3 `simp?` suggested `simp only [implies_true_iff, and.congr_left_iff]`, which didn't work in Lean 3, and `squeeze_simp` suggested `simp only` which (to my mild surprise) does ;-) 3) I also edited the module docstring because I found the Lean 3 docstring claim that a dependent product was "like `α × β`" and then immediately "a generalization of `α ⊕ β`" confusing (these are not the same alpha and beta; the idea is that the first alpha is bool in the second example; hopefully my explanation is now better). Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This PR changes
have's syntax to support all that oflet:The only additional syntax is anonymous
have, which now always has a:before the type (if any) for disambiguation (just likeinstance), and introduces a hypothesisthisas before: