feat(prooflib/fstar): add monadic operators and runners

cryspen · Jan 17, 2024 · 2828612 · 2828612
1 parent 15bbf45
commit 2828612
Show file tree

Hide file tree

Showing 2 changed files with 14 additions and 0 deletions.
diff --git a/proof-libs/fstar/rust_primitives/Rust_primitives.Hax.Control_flow_monad.Moption.fst b/proof-libs/fstar/rust_primitives/Rust_primitives.Hax.Control_flow_monad.Moption.fst
@@ -0,0 +1,7 @@
+module Rust_primitives.Hax.Control_flow_monad.Moption
+
+let run (f: Core.Option.t_Option (Core.Option.t_Option 'a)): Core.Option.t_Option 'a
+    = match f with
+    | Core.Option.Option_Some x -> x 
+    | Core.Option.Option_None -> Core.Option.Option_None
+
diff --git a/proof-libs/fstar/rust_primitives/Rust_primitives.Hax.Control_flow_monad.Mresult.fst b/proof-libs/fstar/rust_primitives/Rust_primitives.Hax.Control_flow_monad.Mresult.fst
@@ -0,0 +1,7 @@
+module Rust_primitives.Hax.Control_flow_monad.Mresult
+
+let run (f: Core.Result.t_Result (Core.Result.t_Result 'a 'e) 'e): Core.Result.t_Result 'a 'e
+    = match f with
+    | Core.Result.Result_Ok x -> x 
+    | Core.Result.Result_Err e -> Core.Result.Result_Err e
+