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 452fe72 commit c381a0cCopy full SHA for c381a0c
src/Init/Data/String/Defs.lean
@@ -457,8 +457,6 @@ def Slice.rawEndPos (s : Slice) : Pos.Raw where
457
@[simp]
458
theorem Slice.byteIdx_rawEndPos {s : Slice} : s.rawEndPos.byteIdx = s.utf8ByteSize := (rfl)
459
460
-
461
462
/-- Criterion for validity of positions in string slices. -/
463
structure Pos.Raw.IsValidForSlice (s : Slice) (p : Pos.Raw) : Prop where
464
le_rawEndPos : p ≤ s.rawEndPos
0 commit comments