From 69a9ea217b55719415e2a5990f3b1e0fb7cd8cdc Mon Sep 17 00:00:00 2001
From: ROMemories <152802150+ROMemories@users.noreply.github.com>
Date: Tue, 10 Sep 2024 09:26:05 +0200
Subject: [PATCH] fix(fstar-core): add support for `Option::map`

---
 proof-libs/fstar/core/Core.Option.fst | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/proof-libs/fstar/core/Core.Option.fst b/proof-libs/fstar/core/Core.Option.fst
index 08d8bed2d..d3c57c44a 100644
--- a/proof-libs/fstar/core/Core.Option.fst
+++ b/proof-libs/fstar/core/Core.Option.fst
@@ -7,6 +7,11 @@ let impl__and_then #t_Self #t (self: t_Option t_Self) (f: t_Self -> t_Option t):
   | Option_Some x -> f x
   | Option_None -> Option_None
 
+let impl__map #t_Self #t (self: t_Option t_Self) (f: t_Self -> t): t_Option t =
+  match self with
+  | Option_Some x -> Option_Some (f x)
+  | Option_None -> Option_None
+
 let impl__unwrap #t (x: t_Option t {Option_Some? x}): t = Option_Some?._0 x
 
 let impl__is_some #t_Self (self: t_Option t_Self): bool =  Option_Some? self