Map Module

src/stdlib/gospelstdlib.mli

@@ -497,6 +497,13 @@ end
 module Map : sig
   (** Maps from keys of type ['a] to values of type ['b] are represented by
       Gospel functions of type ['a -> 'b]. *)
+
+  (*@ type ('a, 'b) t = ('a, 'b) map *)
+
+  (*@ function domain (default : 'b) (m : ('a, 'b) t) : 'a Set.t *)
+
+  (*@ axiom domain_mem :
+        forall x m default. m x <> default -> Set.mem x (domain default m) *)
 end
 
 (* The following modules are deprecated and only exist to ensure the tests pass. In the future, assuming this branch is merged, they should be removed and the tests changed*)

test/typechecker/t1_not_t2.mli

@@ -26,6 +26,6 @@ type 'a t2 = T of 'a * int
    [125] File "t1_not_t2.mli", line 16, characters 8-15:
          16 |       | T (_,y) -> y
                       ^^^^^^^
-         Error: This pattern matches values of type 'a456 t2
+         Error: This pattern matches values of type 'a464 t2
                 but a pattern was expected which matches values of type 'a t1.
    |gospel_expected} *)

test/typechecker/tuple_arity1.mli

@@ -26,6 +26,6 @@ val f : 'a -> 'a
    [125] File "tuple_arity1.mli", line 18, characters 13-20:
          18 |     raises E (x,y,z) -> integer_of_int x = 1 *)
                            ^^^^^^^
-         Error: This pattern matches values of type 'a457 * 'a458 * 'a459
+         Error: This pattern matches values of type 'a465 * 'a466 * 'a467
                 but a pattern was expected which matches values of type int * int.
    |gospel_expected} *)

test/typechecker/tuple_arity2.mli

@@ -22,7 +22,7 @@ val f : 'a -> 'a
    [125] File "tuple_arity2.mli", line 18, characters 13-18:
          18 |     raises E (x,y) -> integer_of_int x = 1
                            ^^^^^
-         Error: This pattern matches values of type 'a456 * 'a457
+         Error: This pattern matches values of type 'a464 * 'a465
                 but a pattern was expected which matches values of type
                 int * int * int.
    |gospel_expected} *)