English
Extend(c) with i: Option(Fin c.length) is defined as ExtendLeft if i = None, else ExtendMiddle i.
Русский
Расширение разбиения c с i: Option(Fin c.length) определено как ExtendLeft при i = None, иначе ExtendMiddle i.
LaTeX
$$$\\text{extend}(c,i) = \\begin{cases} c.extendLeft, & i = \\mathrm{None} \\\\ c.extendMiddle i, & i = \\mathrm{Some}(i) \\end{cases}$$$
Lean4
/-- Extend an ordered partition of `n` entries, by adding singleton to the left or appending it
to one of the existing part. -/
def extend (c : OrderedFinpartition n) (i : Option (Fin c.length)) : OrderedFinpartition (n + 1) :=
match i with
| none => c.extendLeft
| some i => c.extendMiddle i