We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent 7686753 commit a27a825Copy full SHA for a27a825
1 file changed
Binary/Get.lean
@@ -91,7 +91,8 @@ def takeRange (min max : Nat) (p : Get α) : Get (Array α) := do
91
92
@[inline, specialize]
93
def sepBy (x : Get α) (sep : Get Unit) : Get (Array α) := do
94
- let mut t := #[]
+ let some l ← optional x | return #[]
95
+ let mut t := #[l]
96
repeat
97
let some v ← optional (sep *> x) | break
98
t := t.push v
@@ -108,7 +109,8 @@ def sepBy1 (x : Get α) (s : Get Unit) : Get (Array α) := do
108
109
110
111
def sepByUpTo (n : Nat) (x : Get α) (s : Get Unit) : Get (Array α) := do
112
113
114
115
if t.size ≥ n then break
116
let some v ← optional (s *> x) | break
0 commit comments