[Merged by Bors] - chore: clean up evalNot norm_num extension#9532
[Merged by Bors] - chore: clean up evalNot norm_num extension#9532
Conversation
| guard <|← withNewMCtxDepth <| isDefEq α q(Prop) | ||
| let .isBool b p ← derive q($a) | failure | ||
| haveI' : u =QL 0 := ⟨⟩; haveI' : $α =Q Prop := ⟨⟩ | ||
| haveI' : $e =Q ¬ $a := ⟨⟩ |
There was a problem hiding this comment.
Ah, we are trying return a value of type NormNum.Result e, and we do it by analyzing a. The $e =Q ¬ $a thing is so that the typechecker knows how e relates to a.
But then how does this code still work even when I delete these lines? Does that mean there's a bug in Qq?
There was a problem hiding this comment.
(I re-added the lines in 27adfeb, because this seems to me more likely to be a bug in Qq than a problem with the code here.)
There was a problem hiding this comment.
I would have expected that either $e =Q ¬ $a or the cast have p : Q($a) := p would be sufficient. But it seems from d94bd42 that we don't need either. So I'm in favour of removing these again.
On the other hand, I must admit that placating Qq is still a deeply magical process to me so I'm inclined to accept any variation of the code that compiles and looks plausible. So I'll let you decide.
Vierkantor
left a comment
There was a problem hiding this comment.
Nice cleanup!
bors d+
| guard <|← withNewMCtxDepth <| isDefEq α q(Prop) | ||
| let .isBool b p ← derive q($a) | failure | ||
| haveI' : u =QL 0 := ⟨⟩; haveI' : $α =Q Prop := ⟨⟩ | ||
| haveI' : $e =Q ¬ $a := ⟨⟩ |
There was a problem hiding this comment.
I would have expected that either $e =Q ¬ $a or the cast have p : Q($a) := p would be sufficient. But it seems from d94bd42 that we don't need either. So I'm in favour of removing these again.
On the other hand, I must admit that placating Qq is still a deeply magical process to me so I'm inclined to accept any variation of the code that compiles and looks plausible. So I'll let you decide.
|
✌️ dwrensha can now approve this pull request. To approve and merge a pull request, simply reply with |
|
bors r+ |
* Uses `deriveBool`, which was added in #3892, and allows removal of some `have` lines. * Changes an `if then else` into a match. This is more readable in my opinion.
|
Pull request successfully merged into master. Build succeeded: |
* Uses `deriveBool`, which was added in #3892, and allows removal of some `have` lines. * Changes an `if then else` into a match. This is more readable in my opinion.
deriveBool, which was added in [Merged by Bors] - feat: port Data.Nat.PrimeNormNum #3892, and allows removal of somehavelines.if then elseinto a match. This is more readable in my opinion.