Skip to content
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

Port op_induction #4551

Closed
jcommelin opened this issue Jun 1, 2023 · 1 comment
Closed

Port op_induction #4551

jcommelin opened this issue Jun 1, 2023 · 1 comment

Comments

@jcommelin
Copy link
Member

Both the tactic and the attribute
@jcommelin jcommelin mentioned this issue Jun 1, 2023
Closed
@jcommelin jcommelin changed the title Restore op_induction Port op_induction Jun 1, 2023
@semorrison
Copy link
Contributor

I don't think this is actually necessary. I wrote new induction principle, and induction and cases use it by default. So op_induction is not necessary "by hand". If you want aesop to call it I think just attribute [local aesop safe cases] Opposite suffices.

@semorrison semorrison mentioned this issue Jun 14, 2023
Closed
@bors bors bot closed this as completed in 9558b65 Jun 14, 2023
alexkeizer pushed a commit that referenced this issue Jun 22, 2023
@semorrison @alexkeizer
chore: clean up porting notes about op_induction (#5035)
03ab816 
Closes #4551.

Essentially `op_induction` is not necessary, now that `Opposite.rec'` is labelled with `@[eliminator]`. It would be nice if we could use this from inside `aesop`, see leanprover-community/aesop#59.



Co-authored-by: Scott Morrison <scott.morrison@anu.edu.au>
semorrison added a commit that referenced this issue Jun 25, 2023
@semorrison
chore: clean up porting notes about op_induction (#5035)
8c4bb82 
Closes #4551.

Essentially `op_induction` is not necessary, now that `Opposite.rec'` is labelled with `@[eliminator]`. It would be nice if we could use this from inside `aesop`, see leanprover-community/aesop#59.



Co-authored-by: Scott Morrison <scott.morrison@anu.edu.au>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

[Merged by Bors] - chore: clean up porting notes about op_induction leanprover-community/mathlib4
2 participants
@semorrison @jcommelin