English
There is an estimator data for the sum (HAdd) of two thunk estimators, with bound combining pairwise bounds and improvement proceeding first through the first summand, then the second.
Русский
Существует структура оценивателя для суммы двух thunk-оценок, градация границ складывается попарно; сначала улучшается первый слагаемый, затем второй.
LaTeX
$$EstimatorData (a + b) (εa × εb) with bound e := (bound a e.1, bound b e.2) and improve e := if some then update fst else if some then update snd else none$$
Lean4
@[simps]
instance [Add α] {a b : Thunk α} (εa εb : Type*) [EstimatorData a εa] [EstimatorData b εb] :
EstimatorData (a + b) (εa × εb) where
bound e := bound a e.1 + bound b e.2
improve
e :=
match improve a e.1 with
| some e' => some { e with fst := e' }
| none =>
match improve b e.2 with
| some e' => some { e with snd := e' }
| none => none
