From 28286128fb0bdd2d868a96a805edacf1f2b5032c Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Wed, 17 Jan 2024 19:40:33 +0100 Subject: [PATCH] feat(prooflib/fstar): add monadic operators and runners --- .../Rust_primitives.Hax.Control_flow_monad.Moption.fst | 7 +++++++ .../Rust_primitives.Hax.Control_flow_monad.Mresult.fst | 7 +++++++ 2 files changed, 14 insertions(+) create mode 100644 proof-libs/fstar/rust_primitives/Rust_primitives.Hax.Control_flow_monad.Moption.fst create mode 100644 proof-libs/fstar/rust_primitives/Rust_primitives.Hax.Control_flow_monad.Mresult.fst 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 new file mode 100644 index 000000000..30f8a3298 --- /dev/null +++ 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 new file mode 100644 index 000000000..e508ada99 --- /dev/null +++ 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 +