From 23ba24c343adbe3053a7e22df2ad65725dd0be2a Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Fri, 28 Feb 2025 17:58:57 -0500 Subject: [PATCH] Leave `TypeOfIsSound` in that single simp Signed-off-by: Adrian Palacios --- cedar-lean/Cedar/Thm/Validation/Typechecker/Call.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/cedar-lean/Cedar/Thm/Validation/Typechecker/Call.lean b/cedar-lean/Cedar/Thm/Validation/Typechecker/Call.lean index b1b18c3e0..8b91eb399 100644 --- a/cedar-lean/Cedar/Thm/Validation/Typechecker/Call.lean +++ b/cedar-lean/Cedar/Thm/Validation/Typechecker/Call.lean @@ -605,7 +605,7 @@ theorem type_of_call_offset_is_sound {xs : List Expr} {c₁ c₂ : Capabilities} have ⟨dt₁, hr₁⟩ := instance_of_datetime_type_is_datetime hr₁ subst hr₁ have ih₂ := ih x₂ - simp [List.mem_cons, List.mem_singleton, true_or, TypeOfIsSound, forall_const] at ih₂ + simp [TypeOfIsSound] at ih₂ split_type_of h₈ ; rename_i h₈ hl₈ hr₈ have ⟨_, v₂, hl₂, hr₂⟩ := ih₂ h₁ h₂ h₈ simp only [EvaluatesTo] at ih₂