tweak

Signed-off-by: John Kastner <jkastner@amazon.com>
cedar-policy · Mar 6, 2025 · 05784b1 · 05784b1
1 parent b06a6a3
commit 05784b1
Showing 1 changed file with 2 additions and 1 deletion.
diff --git a/cedar-lean/Cedar/Thm/Validation/Levels/CheckLevel.lean b/cedar-lean/Cedar/Thm/Validation/Levels/CheckLevel.lean
@@ -124,7 +124,6 @@ inductive TypedExpr.AtLevel : TypedExpr → Nat → Prop where
     AtLevel (.call xfn args ty) n
 end
 
-mutual
 
 theorem entity_access_at_level_succ {tx : TypedExpr} {n n' : Nat}
   (h₁ : TypedExpr.EntityAccessAtLevel tx n n' path) :
@@ -169,6 +168,8 @@ theorem entity_access_at_level_then_at_level {tx : TypedExpr} {n : Nat} {path :
     | exact entity_access_at_level_then_at_level (by assumption)
 termination_by tx
 
+mutual
+
 theorem entity_access_level_spec {tx : TypedExpr} {n nmax : Nat} {path : List Attr} :
   (TypedExpr.EntityAccessAtLevel tx n nmax path) ↔ (checkEntityAccessLevel tx n nmax path)
 := by