We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
1 parent f082878 commit fc6ea1eCopy full SHA for fc6ea1e
src/Init/Data/String/Basic.lean
@@ -3478,7 +3478,7 @@ where
3478
let spos' := s.str.prev spos
3479
let tpos' := t.str.prev tpos
3480
if s.str.get spos' == t.str.get tpos' then
3481
- have : spos' < spos := s.str.prev_lt_of_pos spos (String.Pos.ne_zero_of_lt h.1)
+ have : spos' < spos := s.str.prev_lt_of_pos spos (String.Pos.Raw.ne_zero_of_lt h.1)
3482
loop spos' tpos'
3483
else
3484
spos
0 commit comments