From 90f7499769c468ab29a933d18243d55bc7e222ce Mon Sep 17 00:00:00 2001
From: ahuoguo <ahuoguo@gmail.com>
Date: Thu, 20 Jul 2023 14:47:39 -0400
Subject: [PATCH] verus doc should be fixxed, map_magic put back

---
 source/pervasive/map.rs | 36 ++++++++++++++++++------------------
 1 file changed, 18 insertions(+), 18 deletions(-)

diff --git a/source/pervasive/map.rs b/source/pervasive/map.rs
index 259f9aba8a..71a18ed74b 100644
--- a/source/pervasive/map.rs
+++ b/source/pervasive/map.rs
@@ -556,6 +556,24 @@ pub proof fn axiom_map_ext_equal_deep<K, V>(m1: Map<K, V>, m2: Map<K, V>)
 {
 }
 
+// auto style axiom bundle
+pub proof fn map_magic<K,V>()
+    ensures
+    forall |fk: FnSpec(K) -> bool, fv: FnSpec(K) -> V| #[trigger] Map::<K,V>::new(fk,fv).dom()
+            == Set::<K>::new(|k: K| fk(k)), //axiom_map_new_domain
+    forall |fk: FnSpec(K) -> bool, fv: FnSpec(K) -> V| #[trigger] Map::<K,V>::new(fk,fv).values() 
+            == Set::<V>::new(|v: V| exists |k: K| #[trigger] fk(k) && #[trigger] fv(k) == v),  //axiom_map_new_values
+{
+    assert forall |fk: FnSpec(K) -> bool, fv: FnSpec(K) -> V| 
+        #[trigger] Map::<K,V>::new(fk,fv).dom() == Set::<K>::new(|k: K| fk(k)) by {
+            axiom_map_new_domain(fk, fv);
+        }
+    assert forall |fk: FnSpec(K) -> bool, fv: FnSpec(K) -> V| #[trigger] Map::<K,V>::new(fk,fv).values() 
+        == Set::<V>::new(|v: V| exists |k: K| #[trigger] fk(k) && #[trigger] fv(k) == v) by {
+            axiom_map_new_values(fk, fv);
+        }
+}
+
 // Macros
 
 #[doc(hidden)]
@@ -674,24 +692,6 @@ macro_rules! assert_maps_equal_internal {
     }
 }
 
-// // auto style axiom bundle
-// pub proof fn map_magic<K,V>()
-//     ensures
-//     forall |fk: FnSpec(K) -> bool, fv: FnSpec(K) -> V| #[trigger] Map::<K,V>::new(fk,fv).dom()
-//             == Set::<K>::new(|k: K| fk(k)), //axiom_map_new_domain
-//     forall |fk: FnSpec(K) -> bool, fv: FnSpec(K) -> V| #[trigger] Map::<K,V>::new(fk,fv).values() 
-//             == Set::<V>::new(|v: V| exists |k: K| #[trigger] fk(k) && #[trigger] fv(k) == v),  //axiom_map_new_values
-// {
-//     assert forall |fk: FnSpec(K) -> bool, fv: FnSpec(K) -> V| 
-//         #[trigger] Map::<K,V>::new(fk,fv).dom() == Set::<K>::new(|k: K| fk(k)) by {
-//             axiom_map_new_domain(fk, fv);
-//         }
-//     assert forall |fk: FnSpec(K) -> bool, fv: FnSpec(K) -> V| #[trigger] Map::<K,V>::new(fk,fv).values() 
-//         == Set::<V>::new(|v: V| exists |k: K| #[trigger] fk(k) && #[trigger] fv(k) == v) by {
-//             axiom_map_new_values(fk, fv);
-//         }
-// }
-
 #[doc(hidden)]
 pub use assert_maps_equal_internal;
 pub use assert_maps_equal;