diff options
Diffstat (limited to 'backends/lean/Base/Primitives/Scalar.lean')
| -rw-r--r-- | backends/lean/Base/Primitives/Scalar.lean | 5 |
1 files changed, 0 insertions, 5 deletions
diff --git a/backends/lean/Base/Primitives/Scalar.lean b/backends/lean/Base/Primitives/Scalar.lean index 014decb1..2bee8a2f 100644 --- a/backends/lean/Base/Primitives/Scalar.lean +++ b/backends/lean/Base/Primitives/Scalar.lean @@ -364,11 +364,6 @@ def Scalar.tryMkOpt (ty : ScalarTy) (x : Int) : Option (Scalar ty) := some (Scalar.ofIntCore x (Scalar.check_bounds_imp_in_bounds h)) else none -def Result.ofOption {a : Type u} (x : Option a) (e : Error) : Result a := - match x with - | some x => ok x - | none => fail e - def Scalar.tryMk (ty : ScalarTy) (x : Int) : Result (Scalar ty) := Result.ofOption (tryMkOpt ty x) integerOverflow |