Merge branch 'main' of https://github.com/reilabs/lampe into us/lens-…

…support
reilabs · Dec 28, 2024 · c8fb45c · c8fb45c
2 parents 5aaf371 + 974f3e3
commit c8fb45c
Showing 1 changed file with 3 additions and 0 deletions.
diff --git a/Lampe/Lampe/Tactic/SeparationLogic.lean b/Lampe/Lampe/Tactic/SeparationLogic.lean
@@ -564,6 +564,7 @@ macro "stephelper1" : tactic => `(tactic|(
     | apply nested_triple STHoare.callLambda_intro
     | apply lam_intro
     | apply cast_intro
+    | apply cast_intro
     | apply callTrait_intro
     | apply callDecl_intro
     -- memory
@@ -586,6 +587,7 @@ macro "stephelper1" : tactic => `(tactic|(
     -- equality
     | apply unitEq_intro
     | apply bEq_intro
+    | apply bEq_intro
     | apply fEq_intro
     | apply uEq_intro
     | apply iEq_intro
@@ -725,6 +727,7 @@ macro "stephelper3" : tactic => `(tactic|(
     -- equality
     | apply ramified_frame_top unitEq_intro
     | apply ramified_frame_top bEq_intro
+    | apply ramified_frame_top bEq_intro
     | apply ramified_frame_top fEq_intro
     | apply ramified_frame_top uEq_intro
     | apply ramified_frame_top iEq_intro