chore(Util/StubLinter): correctly handle Prop-valued instances - #5071
chore(Util/StubLinter): correctly handle Prop-valued instances#5071YaelDillies wants to merge 1 commit into
Conversation
These should not be considered stub definitions since they are Prop-valued.
| rational points is torsion, not that it is of infinite rank. -/ | ||
| @[category research solved, AMS 11 14] | ||
| theorem mordell_weil {K} [Field K] [NumberField K] [DecidableEq K] (E : WeierstrassCurve K) | ||
| instance mordell_weil {K} [Field K] [NumberField K] [DecidableEq K] (E : WeierstrassCurve K) |
There was a problem hiding this comment.
Hm I think at one point we decided that instance shouldn't have a category tag (i.e. problems can't be stated as instances). Should we go back on this?
There was a problem hiding this comment.
Where did this discussion happen?
There was a problem hiding this comment.
Don't know where this discussion happen, but there might be downstream stuff that expects it (which could also be fixed) For instance (no pun intended) I don't even know if the extract_names script handles it correctly.
In any case it can be easily avoided in all instances, right? By preluding it with a named theorem
@[category research solved]
theorem foo : bar := by
sorry
instance bar := foo
So we could lint for and forbid category tags for instances without loosing anything (except possibly convenience)
There was a problem hiding this comment.
I think this happened in gChat (possibly DMs between me and Moritz) about a year ago or even longer!
There was a problem hiding this comment.
I don't really mind, but what's your rationale for disallowing this? that statements with a category tag should be called explicitly?
There was a problem hiding this comment.
One idea to have names to statements is: When people start solving them (and keep track in the future lean-lang/eval for example, but really whereever) is easier to refer to them if they have a name
There was a problem hiding this comment.
Sure, but that's an argument against unnamed instances, not against instances? Paul told me privately that a reason was that our statement extraction used to perform badly on instances. Has that changed?
3 participants
These should not be considered stub definitions since they are Prop-valued.