[Merged by Bors] - fix(tactic/{norm_num, abel}): do not do syntactic matches on typeclass instances #18129
Conversation
eric-wieser
added
bug
awaiting-review
eric-wieser
changed the title
src/tactic/abel.lean
Outdated
| @@ -189,8 +189,12 @@ meta def eval_neg (c : context) : normal_expr → tactic (normal_expr × expr) | |||
| return (term' c (n', -n.2) x a', | |||
| c.app ``term_neg c.inst [n.1, x, a, n', a', h₁, h₂]) | |||
|
|
|||
| def smul {α} [add_comm_monoid α] (n : ℕ) (x : α) : α := n • x | |||
| def smulg {α} [add_comm_group α] (n : ℤ) (x : α) : α := n • x | |||
| @[nolint doc_blame] def nat_smul_inst {α} [add_comm_monoid α] : has_smul ℕ α := by apply_instance | |||
There was a problem hiding this comment.
don't use nolint doc_blame, these should be in the nolints.json file (or documented).
There was a problem hiding this comment.
I'm confused, I thought nolint doc_blame was "this isn't deserving of documentation" whereas nolints.json is "I can't be bothered to document this.
These are not declarations that are intended as API; they only exist because it's easier/faster to construct terms with def than from within the meta code.
How do you feel about me just making them private? They're not something we want in the docs anyway, are they?
There was a problem hiding this comment.
Ah, private doesn't work with the name mangling. I've done what you suggest since it's consistent with how the rest of this file is handled.
I'd still argue that nolinting all of these helper declarations is the right thing to do, but not in this PR.
There was a problem hiding this comment.
I'm confused, I thought
nolint doc_blamewas "this isn't deserving of documentation" whereasnolints.jsonis "I can't be bothered to document this.
I agree with this characterization. They are implementation details (a property they share with most declarations in this file) but the need for them is deserving of documentation.
There was a problem hiding this comment.
but the need for them is deserving of documentation.
Indeed; probably as a library note. Maybe something like
-- see not [declarations for tactics] for an explanation of the lemmas and defs in this section
namespace _helpers
end _helpers
since I think the _ prefix will rightly exclude them from doc-gen.
|
bors r+ |
github-actions
bot
added
ready-to-merge
…s instances (#18129) Specifically, this remove syntactic matches on `has_pow` and `has_smul` instances in favor of unification. In all cases there is a cache we can exploit to avoid looking up the preferred instance from scratch every time.
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
Specifically, this remove syntactic matches on
has_powandhas_smulinstances in favor of unification.In all cases there is a cache we can exploit to avoid looking up the preferred instance from scratch every time.