From 46d53c02a97601e157bf73d1be558390c0752b7e Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond <guillaume.melquiond@inria.fr>
Date: Wed, 30 Oct 2024 17:24:06 +0100
Subject: [PATCH] Mark some types as having an extensional equality.

---
 stdlib/bag.mlw      | 2 ++
 stdlib/bv.mlw       | 2 ++
 stdlib/fmap.mlw     | 2 ++
 stdlib/mach/int.mlw | 2 ++
 stdlib/map.mlw      | 2 ++
 stdlib/set.mlw      | 4 ++++
 stdlib/string.mlw   | 2 ++
 7 files changed, 16 insertions(+)

diff --git a/stdlib/bag.mlw b/stdlib/bag.mlw
index 3eec1e0fb..47afaec30 100644
--- a/stdlib/bag.mlw
+++ b/stdlib/bag.mlw
@@ -25,6 +25,8 @@ module Bag
 
   axiom bag_extensionality: forall a b: bag 'a. a == b -> a = b
 
+  meta extensionality predicate (==)
+
   (** basic constructors of bags *)
 
   function empty_bag: bag 'a
diff --git a/stdlib/bv.mlw b/stdlib/bv.mlw
index 7b812fd83..0aee0f051 100644
--- a/stdlib/bv.mlw
+++ b/stdlib/bv.mlw
@@ -587,6 +587,8 @@ let predicate sle (v1 v2 : t) =
     forall x y : t [x == y]. x == y -> x = y
   meta "remove_unused:dependency" axiom Extensionality, predicate (==)
 
+  meta extensionality predicate (==)
+
   val eq (v1 v2 : t) : bool
     ensures { result <-> v1 = v2 }
 
diff --git a/stdlib/fmap.mlw b/stdlib/fmap.mlw
index 01dcdee94..26238a825 100644
--- a/stdlib/fmap.mlw
+++ b/stdlib/fmap.mlw
@@ -26,6 +26,8 @@ module Fmap
   axiom extensionality:
     forall m1 m2: fmap 'k 'v. m1 == m2 -> m1 = m2
 
+  meta extensionality predicate (==)
+
   predicate mem (k: 'k) (m: fmap 'k 'v) =
     S.mem k m.domain
 
diff --git a/stdlib/mach/int.mlw b/stdlib/mach/int.mlw
index ee3257b34..3c707a2cc 100644
--- a/stdlib/mach/int.mlw
+++ b/stdlib/mach/int.mlw
@@ -77,6 +77,8 @@ module Bounded_int
 
   axiom extensionality: forall x y: t. to_int x = to_int y -> x = y
 
+  meta extensionality function to_int
+
   val (=) (a:t) (b:t) : bool
     ensures { result <-> a = b }
     ensures { to_int a = to_int b -> result }
diff --git a/stdlib/map.mlw b/stdlib/map.mlw
index dab86bdab..d60575c68 100644
--- a/stdlib/map.mlw
+++ b/stdlib/map.mlw
@@ -36,6 +36,8 @@ module MapExt
   (* This lemma is actually provable in Why3, because of how
      eliminate_epsilon handles equality to a lambda-term. *)
 
+  meta extensionality predicate (==)
+
 end
 
 (** {2 Sorted Maps (indexed by integers)} *)
diff --git a/stdlib/set.mlw b/stdlib/set.mlw
index 70e8e039e..0ed7a2886 100644
--- a/stdlib/set.mlw
+++ b/stdlib/set.mlw
@@ -38,6 +38,8 @@ module Set
   lemma extensionality:
     forall s1 s2: set 'a. s1 == s2 -> s1 = s2
 
+  meta extensionality predicate (==)
+
   (** inclusion *)
   predicate subset (s1 s2: set 'a) = forall x : 'a. mem x s1 -> mem x s2
 
@@ -270,6 +272,8 @@ module Fset
   lemma extensionality:
     forall s1 s2: fset 'a. s1 == s2 -> s1 = s2
 
+  meta extensionality predicate (==)
+
   (** inclusion *)
   predicate subset (s1 s2: fset 'a) = forall x : 'a. mem x s1 -> mem x s2
 
diff --git a/stdlib/string.mlw b/stdlib/string.mlw
index 7302ef10f..88d996180 100644
--- a/stdlib/string.mlw
+++ b/stdlib/string.mlw
@@ -439,6 +439,8 @@ module Char
   axiom extensionality [@W:non_conservative_extension:N]:
     forall s1 s2. eq_string s1 s2 -> s1 = s2
 
+  meta extensionality predicate eq_string
+
   function make (size: int) (v: char) : string
 
   axiom make_length: forall size v. size >= 0 ->
-- 
2.11.4.GIT