tidy

Signed-off-by: John Kastner <[email protected]>
cedar-policy · Aug 23, 2024 · 51a78c1 · 51a78c1
1 parent 5893bdc
commit 51a78c1
Show file tree

Hide file tree

Showing 3 changed files with 4 additions and 3 deletions.
diff --git a/cedar-lean/Cedar/Thm/Validation/Typechecker/GetAttr.lean b/cedar-lean/Cedar/Thm/Validation/Typechecker/GetAttr.lean
@@ -192,8 +192,9 @@ theorem type_of_getAttr_is_sound_for_ea_maps {x₁ : Expr} {a : Attr} {c₁ c₁
     rw [h₁₁] at h₈
     contradiction
   case some =>
+    simp only [h₈, getAttr, attrsOf, Map.findOrErr, Except.bind_ok, Except.ok.injEq, false_or, exists_eq_left']
     injections _ h₂
-    simp [←h₂, h₈, getAttr, attrsOf, Map.findOrErr, Except.bind_ok, Except.ok.injEq, false_or, exists_eq_left']
+    rw [←h₂]
     exact instance_of_ea_map_attribute_type h₅ h₈
 
 theorem type_of_getAttr_is_sound {x₁ : Expr} {a : Attr} {c₁ c₂ : Capabilities} {env : Environment} {ty : CedarType} {request : Request} {entities : Entities}

diff --git a/cedar-lean/Cedar/Thm/Validation/Typechecker/Types.lean b/cedar-lean/Cedar/Thm/Validation/Typechecker/Types.lean
@@ -347,7 +347,7 @@ theorem instance_of_record_nil :
 theorem instance_of_attribute_map_nil (ty : CedarType) :
   InstanceOfType (Value.record (Map.mk [])) (CedarType.attribute_map ty)
 := by
-  apply InstanceOfType.instance_of_ea_map<;>
+  apply InstanceOfType.instance_of_ea_map <;>
   simp [Map.find?, List.find?]
 
 theorem instance_of_record_cons {hd : Attr × Qualified CedarType} {tl : List (Attr × Qualified CedarType)} {rhd : Value} {rtl : List (Attr × Value)}

diff --git a/cedar-lean/Cedar/Validation/Typechecker.lean b/cedar-lean/Cedar/Validation/Typechecker.lean
@@ -70,8 +70,8 @@ def typeOfIf (r₁ : CedarType × Capabilities) (r₂ r₃ : ResultType) : Resul
     let (ty₃, c₃) ← r₃
     match ty₂ ⊔ ty₃ with
     | .some (.attribute_map aty) => .error (.unexpectedType aty.attribute_map)
-    | .none => err (.lubErr ty₂ ty₃)
     | .some ty => ok ty ((c₁ ∪ c₂) ∩ c₃)
+    | .none => err (.lubErr ty₂ ty₃)
   | (ty₁, _) => err (.unexpectedType ty₁)
 
 def typeOfAnd (r₁ : CedarType × Capabilities) (r₂ : ResultType) : ResultType :=