-
Notifications
You must be signed in to change notification settings - Fork 298
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(tactic/mk_iff_of_inductive_prop): mk_iff attribute #4863
Conversation
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.
Thanks, this is a good idea!
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.
Thanks for the comments! The last undocumented functions are the ones doing most of the work, so it'd be good to document them now.
@[nolint doc_blame] -- TODO: document | ||
meta def constr_to_prop (univs : list level) (g : list expr) (idxs : list expr) (c : name) : |
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.
Any docstring suggestions?
@[nolint doc_blame] -- TODO: document | ||
meta def to_cases (s : list $ list (option expr) × (expr ⊕ ℕ)) : tactic unit := |
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.
Any docstring suggestions?
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.
These will take some studying to figure out, and I don't think we'll get the original author to chime in. I don't mind leaving it nolint
ed for now, and doing that studying if and when it's necessary.
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.
OK, fair enough. I'd be OK merging this for now then.
@[nolint doc_blame] -- TODO: document | ||
meta def to_inductive | ||
(cs : list name) (gs : list expr) (s : list (list (option expr) × (expr ⊕ ℕ))) (h : expr) : | ||
tactic unit := |
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.
Any docstring suggestions?
bors merge |
This attribute should make `mk_iff_of_inductive_prop` easier to use.
Pull request successfully merged into master. Build succeeded: |
This attribute should make
mk_iff_of_inductive_prop
easier to use.Should
mk_iff
get some more config options?Zulip thread.