diff options
Diffstat (limited to 'backends/lean/Base/Primitives/Base.lean')
| -rw-r--r-- | backends/lean/Base/Primitives/Base.lean | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/backends/lean/Base/Primitives/Base.lean b/backends/lean/Base/Primitives/Base.lean index 4c5b2795..ac4fd340 100644 --- a/backends/lean/Base/Primitives/Base.lean +++ b/backends/lean/Base/Primitives/Base.lean @@ -76,6 +76,11 @@ def eval_global {α: Type u} (x: Result α) (_: ok? x := by prove_eval_global) : | fail _ | div => by contradiction | ok x => x +def Result.ofOption {a : Type u} (x : Option a) (e : Error) : Result a := + match x with + | some x => ok x + | none => fail e + /- DO-DSL SUPPORT -/ def bind {α : Type u} {β : Type v} (x: Result α) (f: α → Result β) : Result β := |