Skip to content

Commit 7686753

Browse files
committed
feat: DecodeResult.toExceptString
1 parent 03ed2af commit 7686753

1 file changed

Lines changed: 6 additions & 0 deletions

File tree

Binary/Basic.lean

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -42,6 +42,12 @@ def DecodeResult.toExcept : DecodeResult α → Except DecodeError α
4242
| .error err _ => .error err
4343
| .pending _ => .error (.userError "pending input")
4444

45+
@[always_inline]
46+
def DecodeResult.toExceptString : DecodeResult α → Except String α
47+
| .success x _ => .ok x
48+
| .error err _ => .error s!"{err}"
49+
| .pending _ => .error "pending input"
50+
4551
@[expose]
4652
def Get (α : Type) : Type := Decoder → (DecodeResult α)
4753

0 commit comments

Comments
 (0)