fix: derive BEq on structure with Prop-fields
#3191
Conversation
arthur-adjedj
changed the title
derive BEq on structure with Prop-fields.derive BEq on structure with Prop-fields
github-actions
bot
added
the
toolchain-available
src/Lean/Elab/Deriving/BEq.lean
Outdated
| let isProof := (← inferType (← inferType x)).isProp | ||
| if isProof then | ||
| continue | ||
| if (← inferType x).isAppOf indVal.name then | ||
| rhs ← `($rhs && $(mkIdent auxFunName):ident $a:ident $b:ident) | ||
| else |
There was a problem hiding this comment.
This is running inferType twice; maybe store as xType and reuse?
Also, maybe use xType.isProof:
lean4/src/Lean/Meta/InferType.lean
Lines 311 to 315 in b614ff1
There was a problem hiding this comment.
Thanks for pointing it out. Looking that the code for isProof, I believe it should be isProp xType and not xType.isProof.
(Sidenote : there are two isProp in practice, Expr.isProp returns true when the given expr is syntactically Prop, whereas Meta.isProp returns true is the expression lives in Prop, this is confusing IMO).
Since similar code was present in DecEq.lean, I've taken the liberty of using Meta.isProp there too.
There was a problem hiding this comment.
Ah, I guess I meant isProof x? Not sure if it’s better if you have to run inferType x later anyways.
There was a problem hiding this comment.
An good point about Meta.isProp and isProp. This is very confusing indeed, but I think you got it right :-)
There was a problem hiding this comment.
My thought process is that isProofQuick and isPropQuick are very similar, and should be comparable in terms of performance. However, if isProofQuick fails, it will have to infer the type, and call isPropQuick afterwards. since inferType x is already called once, I believe using isProp to be more efficient here.
leanprover-community-mathlib4-bot
added
the
builds-mathlib
|
Mathlib CI status (docs):
|
Co-authored-by: Joachim Breitner <[email protected]>
|
Perfect. Thanks for having taken the time to review this :-) |
Closes #3140