-
Notifications
You must be signed in to change notification settings - Fork 251
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.Fin.Tuple.Basic #1516
Conversation
Why is there "attempt 2" in the PR title? It shouldn't stay there when we merge this. |
Reiterating the message from the porting wiki, I would prefer that we get leanprover-community/mathlib#10346 in first, as this change the file and the things it depends on a fair bit. |
-- Porting note: I made this noncomputable because Lean seemed to think it should be | ||
/-- Adding an element at the beginning of an `n`-tuple, to get an `n+1`-tuple. -/ | ||
noncomputable def cons (x : α 0) (p : ∀ i : Fin n, α i.succ) : ∀ i, α i := fun j ↦ Fin.cases x p j | ||
#align fin.cons Fin.cons |
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.
Is there a lean issue tracking this? It seems bizarre that SomeInductive.cases
is noncomputable when the equation compiler is happy to produce something computable.
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.
The compiler ignores the actual Lean term generated by pattern matching and just compiles the pattern matching directly. I'm sure it's on the todo list of the developers.
When I first tried porting this (#1515) I got a strange error where |
My bad; I didn't see that message. |
For the record, we discussed this on zulip and ended up not waiting for this, because mathlib3port is not being updated right now. I'm happy to help re-port once it's back up (though you may need to remind me). |
bors r+ |
Co-authored-by: qawbecrdtey <40463813+qawbecrdtey@users.noreply.github.com> Co-authored-by: Johan Commelin <johan@commelin.net> Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Pull request successfully merged into master. Build succeeded: |
Co-authored-by: qawbecrdtey <40463813+qawbecrdtey@users.noreply.github.com> Co-authored-by: Johan Commelin <johan@commelin.net> Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Should maybe wait for
fin.append
tomatrix.vec_append
, introduce a newfin.append
andfin.repeat
. mathlib#10346