tidy

Signed-off-by: John Kastner <jkastner@amazon.com>
cedar-policy · Mar 6, 2025 · f040b7c · f040b7c
1 parent 5052af2
commit f040b7c
Show file tree

Hide file tree

Showing 2 changed files with 1 addition and 4 deletions.
diff --git a/cedar-lean/Cedar/Thm/Validation/Typechecker/And.lean b/cedar-lean/Cedar/Thm/Validation/Typechecker/And.lean
@@ -103,11 +103,10 @@ theorem type_of_and_is_sound {x₁ x₂ : Expr} {c₁ c₂ : Capabilities} {env
     have h₇ := instance_of_ff_is_false ih₁₃
     simp at h₇ ; subst h₇
     simp [EvaluatesTo] at ih₁₂
-    exists (.prim (.bool false))
-    apply (And.intro · false_is_instance_of_ff)
     rcases ih₁₂ with ih₁₂ | ih₁₂ | ih₁₂ | ih₁₂ <;>
     simp [EvaluatesTo, evaluate, Result.as, ih₁₂, Coe.coe, Value.asBool] <;>
     try exact type_is_inhabited (CedarType.bool BoolType.ff)
+    exact false_is_instance_of_ff
   case isFalse h₇ =>
     replace ⟨bty, tx₂, bty₂, rc₂, htx, htx₂, hty₂, h₆⟩ := h₆
     split at h₆ <;> have ⟨hbty, hc⟩ := h₆ <;> subst bty c₂ tx

diff --git a/cedar-lean/Cedar/Thm/Validation/Typechecker/UnaryApp.lean b/cedar-lean/Cedar/Thm/Validation/Typechecker/UnaryApp.lean
@@ -75,8 +75,6 @@ theorem type_of_not_inversion {x₁ : Expr} {c₁ c₂ : Capabilities} {env : En
         simp only [TypedExpr.typeOf]
         simp [ResultType.typeOf, Except.map, h'₁]
 
-
-
 theorem type_of_not_is_sound {x₁ : Expr} {c₁ c₂ : Capabilities} {env : Environment} {ty : TypedExpr} {request : Request} {entities : Entities}
   (h₁ : CapabilitiesInvariant c₁ request entities)
   (h₂ : RequestAndEntitiesMatchEnvironment env request entities)