rename filenames

verus-lang · Mar 28, 2024 · d10b874 · d10b874
1 parent 4b98f2d
commit d10b874
Show file tree

Hide file tree

Showing 13 changed files with 22 additions and 22 deletions.
diff --git a/crates/ide-assists/src/handlers/proof_action.rs b/crates/ide-assists/src/handlers/proof_action.rs
@@ -1,18 +1,18 @@
-pub(crate) mod assert_by;
-pub(crate) mod intro_failing_ensures;
-pub(crate) mod intro_failing_requires;
-pub(crate) mod intro_match;
-pub(crate) mod localize_error;
-pub(crate) mod remove_dead_assertion;
+pub(crate) mod insert_assert_by_block;
+pub(crate) mod insert_failing_postcondition;
+pub(crate) mod insert_failing_precondition;
+pub(crate) mod intro_matching_assertions;
+pub(crate) mod decompose_failing_assert;
+pub(crate) mod remove_redundant_assertion;
 pub(crate) mod apply_induction;
-pub(crate) mod wp_move_assertion;
-pub(crate) mod assert_by_reveal;
-pub(crate) mod insert_reveal;
-pub(crate) mod imply_to_if;
+pub(crate) mod weakest_pre_step;
+pub(crate) mod reveal_opaque_in_by_block;
+pub(crate) mod reveal_opaque_above;
+pub(crate) mod convert_imply_to_if;
 pub(crate) mod split_imply_ensures;
 pub(crate) mod intro_forall;
 pub(crate) mod intro_forall_implies;
-pub(crate) mod by_assume_false;
+pub(crate) mod intro_assume_false;
 pub(crate) mod split_smaller_or_equal_to;
 pub(crate) mod seq_index_inbound;
 
diff --git a/.../src/handlers/proof_action/imply_to_if.rs → ...dlers/proof_action/convert_imply_to_if.rs b/.../src/handlers/proof_action/imply_to_if.rs → ...dlers/proof_action/convert_imply_to_if.rs
diff --git a/...c/handlers/proof_action/localize_error.rs → .../proof_action/decompose_failing_assert.rs b/...c/handlers/proof_action/localize_error.rs → .../proof_action/decompose_failing_assert.rs
diff --git a/...ts/src/handlers/proof_action/assert_by.rs → ...rs/proof_action/insert_assert_by_block.rs b/...ts/src/handlers/proof_action/assert_by.rs → ...rs/proof_action/insert_assert_by_block.rs
diff --git a/...ers/proof_action/intro_failing_ensures.rs → ...of_action/insert_failing_postcondition.rs b/...ers/proof_action/intro_failing_ensures.rs → ...of_action/insert_failing_postcondition.rs
diff --git a/...rs/proof_action/intro_failing_requires.rs → ...oof_action/insert_failing_precondition.rs b/...rs/proof_action/intro_failing_requires.rs → ...oof_action/insert_failing_precondition.rs
diff --git a/.../handlers/proof_action/by_assume_false.rs → ...ndlers/proof_action/intro_assume_false.rs b/.../handlers/proof_action/by_assume_false.rs → ...ndlers/proof_action/intro_assume_false.rs
diff --git a/.../src/handlers/proof_action/intro_match.rs → ...proof_action/intro_matching_assertions.rs b/.../src/handlers/proof_action/intro_match.rs → ...proof_action/intro_matching_assertions.rs
diff --git a/...ers/proof_action/remove_dead_assertion.rs → ...roof_action/remove_redundant_assertion.rs b/...ers/proof_action/remove_dead_assertion.rs → ...roof_action/remove_redundant_assertion.rs
diff --git a/...rc/handlers/proof_action/insert_reveal.rs → ...dlers/proof_action/reveal_opaque_above.rs b/...rc/handlers/proof_action/insert_reveal.rs → ...dlers/proof_action/reveal_opaque_above.rs
diff --git a/...handlers/proof_action/assert_by_reveal.rs → ...proof_action/reveal_opaque_in_by_block.rs b/...handlers/proof_action/assert_by_reveal.rs → ...proof_action/reveal_opaque_in_by_block.rs
diff --git a/...andlers/proof_action/wp_move_assertion.rs → ...handlers/proof_action/weakest_pre_step.rs b/...andlers/proof_action/wp_move_assertion.rs → ...handlers/proof_action/weakest_pre_step.rs
diff --git a/crates/ide-assists/src/lib.rs b/crates/ide-assists/src/lib.rs
@@ -365,21 +365,21 @@ pub(crate) mod handlers {
             // sorted list above?
             //
             // Verus
-            proof_action::assert_by::assert_by,
-            proof_action::intro_failing_ensures::intro_failing_ensures,
-            proof_action::intro_failing_requires::intro_failing_requires,
-            proof_action::intro_match::intro_match,
-            proof_action::wp_move_assertion::wp_move_assertion,
+            proof_action::insert_assert_by_block::assert_by,
+            proof_action::insert_failing_postcondition::intro_failing_ensures,
+            proof_action::insert_failing_precondition::intro_failing_requires,
+            proof_action::intro_matching_assertions::intro_match,
+            proof_action::weakest_pre_step::wp_move_assertion,
             proof_action::apply_induction::apply_induction,
-            proof_action::localize_error::localize_error,
-            proof_action::remove_dead_assertion::remove_dead_assertions,
-            proof_action::assert_by_reveal::assert_by_reveal,
-            proof_action::insert_reveal::insert_reveal,
-            proof_action::imply_to_if::imply_to_if,
+            proof_action::decompose_failing_assert::localize_error,
+            proof_action::remove_redundant_assertion::remove_dead_assertions,
+            proof_action::reveal_opaque_in_by_block::assert_by_reveal,
+            proof_action::reveal_opaque_above::insert_reveal,
+            proof_action::convert_imply_to_if::imply_to_if,
             proof_action::split_imply_ensures::split_imply_ensures,
             proof_action::intro_forall::intro_forall,   
             proof_action::intro_forall_implies::intro_forall_implies,
-            proof_action::by_assume_false::by_assume_false,
+            proof_action::intro_assume_false::by_assume_false,
             proof_action::split_smaller_or_equal_to::split_smaller_or_equal_to,
             proof_action::seq_index_inbound::seq_index_inbound,
         ]