fix(fstar-core): add support for Option::map

hacspec · Sep 10, 2024 · 69a9ea2 · 69a9ea2
1 parent 5ac5c22
commit 69a9ea2
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