English
lower computes the sequence of differences of a given list with respect to a baseline n: lower [a1, a2, ...] n = [a1 - n, a2 - a1, ...].
Русский
lower вычисляет последовательность разностей исходного списка относительно базового значения n: lower [a1, a2, ...] n = [a1 − n, a2 − a1, ...].
LaTeX
$$$\\operatorname{lower}: \\text{List }\\mathbb{N} \\to \\mathbb{N} \\to \\text{List }\\mathbb{N},\\quad \\operatorname{lower}([] , _) = [],\\quad \\operatorname{lower}(m::l, n) = (m-n) :: \\operatorname{lower}(l, m).$$$
Lean4
/-- Outputs the list of differences of the input list, that is
`lower [a₁, a₂, ...] n = [a₁ - n, a₂ - a₁, ...]` -/
def lower : List ℕ → ℕ → List ℕ
| [], _ => []
| m :: l, n => (m - n) :: lower l m
