Merge branch 'main' into fold-step-boundary

hacspec · Sep 11, 2024 · 172bd8a · 172bd8a
2 parents 0e95327 + 5e3e6d2
commit 172bd8a
Showing 1 changed file with 5 additions and 0 deletions.
diff --git 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