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.
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
[Merged by Bors] - feat: port Data.Stream.Init #849
Conversation
Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk>
Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk>
Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk>
Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Should the file |
No, unless it is moved in lean 3 as well. It is a lean 3 core file but it's not in |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This is great. A bunch of auto-ported proofs didn't work for you because rw [def]
seems to behave differently in Lean 4, in the middle of a proof involved in a definition of def
. I looked at your workarounds and fed some additional information into the rewrites and got them working again; as a result I could golf a bunch of your proofs back to versions which far more closely approximate the autoported versions. Not a big deal but I thought you might be interested! Whether or not you add these golfs, this PR is ready to merge.
Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk>
Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk>
Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk>
Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk>
Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk>
Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk>
Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk>
Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk>
Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk>
…unity/mathlib4 into data_stream_init
bors merge |
e574b1a4e891376b0ef974b926da39e05da12a06 Due to name collisions with `Stream` in Lean 4, the structure is `Stream'` as earlier defined. Recursive proofs were changed a bit to show termination. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Pull request successfully merged into master. Build succeeded:
|
e574b1a4e891376b0ef974b926da39e05da12a06
Due to name collisions with
Stream
in Lean 4, the structure isStream'
as earlier defined. Recursive proofs were changed a bit to show termination.