verus doc should be fixxed, map_magic put back

verus-lang · Jul 20, 2023 · 90f7499 · 90f7499
1 parent 5924ebf
commit 90f7499
Showing 1 changed file with 18 additions and 18 deletions.
diff --git 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;