fix: prefer longer parse even if unsuccessful #1658
Conversation
src/Init/Data/Ord.lean
Outdated
| @@ -59,6 +59,10 @@ instance : Ord USize where | |||
| instance : Ord Char where | |||
| compare x y := compareOfLessAndEq x y | |||
|
|
|||
| instance lexOrd [Ord α] [Ord β] : Ord (α × β) where | |||
There was a problem hiding this comment.
I'd prefer if we didn't make this a global instance. It conflicts with the general pointwise order instance which works more generally for preorders as well.
There was a problem hiding this comment.
Yeah, I thought we had discussed this instance before and was quite confused that it did not exist at all (but I may have confused it with the general Ord/LT diamond discussion).
Kha
force-pushed
the
longest-parse-prio
branch
from
55e1f5b to
cb9e35f
Compare
| @@ -1424,7 +1424,7 @@ def longestMatchStep (left? : Option Syntax) (startSize startLhsPrec : Nat) (sta | |||
| let prevLhsPrec := s.lhsPrec | |||
| let s := s.restore prevSize startPos | |||
| let s := runLongestMatchParser left? startLhsPrec p c s | |||
| match compare previousScore (score s prio) with | |||
| match (let _ := @lexOrd; compare previousScore (score s prio)) with | |||
There was a problem hiding this comment.
Is this the correct idiom then :) ?
There was a problem hiding this comment.
You can also do local attribute [instance] lexOrd before the function, or have a type alias Lex A B on which to unconditionally put the instance. But this way is fine too, or (inst := lexOrd) in compare. If this program were subject to proofs I would generally prefer haveI here to avoid creating the additional let binding in the generated term, but for this code that's not really a concern and the compiler will normalize the two variants the same anyway.
There was a problem hiding this comment.
I will merge as-is. I think the haveI/letI remark is important, we should discuss it in the next dev-meeting. We also get back to the let vs let dep discussion. It would be great to use the same style for letI (let inl?), and have it as part of the let family: let, let rec, let dep, let mut, ...
As mentioned in https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/.22have.22.20with.20tactic-mode.20proof/near/300188387