renamed utkans_thm to nested_triple

reilabs · Nov 27, 2024 · 0edfe4b · 0edfe4b
1 parent 284c344
commit 0edfe4b
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 4 deletions.
diff --git a/Lampe/Lampe/Hoare/SepTotal.lean b/Lampe/Lampe/Hoare/SepTotal.lean
@@ -91,9 +91,7 @@ theorem consequence_frame_left {H H₁ H₂ : SLP (State p)}
   rw [SLP.star_comm]
   apply SLP.ent_star_top
 
-
--- [TODO] find a better name for this
-theorem utkans_thm {Q : _ → SLP (State p)}
+theorem nested_triple {Q : _ → SLP (State p)}
   (h_hoare_imp : STHoare p Γ P e₁ Q → STHoare p Γ (P ⋆ H) e₂ (fun v => Q v ⋆ H))
   (h_hoare : STHoare p Γ P e₁ Q)
   (h_ent_pre : H ⊢ P ⋆ H) :

diff --git a/Lampe/Lampe/Tactic/SeparationLogic.lean b/Lampe/Lampe/Tactic/SeparationLogic.lean
@@ -516,7 +516,7 @@ macro "stephelper1" : tactic => `(tactic|(
     | apply fresh_intro
     | apply assert_intro
     | apply skip_intro
-    | apply STHoare.utkans_thm STHoare.callLambda_intro
+    | apply STHoare.nested_triple STHoare.callLambda_intro
     | apply lam_intro
     -- memory builtins
     | apply var_intro