We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent 82dd360 commit 86f4127Copy full SHA for 86f4127
cedar-lean/Cedar/Thm/TPE/BatchedEvaluator.lean
@@ -80,8 +80,8 @@ theorem entities_refine_withMissing_asPartial_append (es : Entities) (m2 m1 : Sl
80
exact h1 a e₁'.asPartial h_find₂
81
| none =>
82
have h_find₃ : m1.asPartial.find? a = none := by
83
- unfold EntitiesWithMissing.asPartial
84
- exact Map.find?_mapOnValues_none EntityOrMissing.asPartial h_case
+ unfold SlicedEntities.asPartial
+ exact Map.find?_mapOnValues_none MaybeEntityData.asPartial h_case
85
rw [h_find₃] at h_find
86
simp [Option.or] at h_find
87
exact h2 a e₂ h_find
0 commit comments