English
shiftLeft' b m n performs a left shift of m, n times, inserting bit b as the least significant bit each time.
Русский
shiftLeft' b m n выполняет левый сдвиг m на n раз, каждый раз вставляя бит b в младшие разряды.
LaTeX
$$$\mathrm{shiftLeft'}(b, m, n) \text{ is defined by } \begin{cases} \mathrm{shiftLeft'}(b,m,0) = m, \\ \mathrm{shiftLeft'}(b,m,n+1) = \mathrm{bit}(b, \mathrm{shiftLeft'}(b,m,n)). \end{cases}$$$
Lean4
/-- `shiftLeft' b m n` performs a left shift of `m` `n` times
and adds the bit `b` as the least significant bit each time.
Returns the corresponding natural number -/
def shiftLeft' (b : Bool) (m : ℕ) : ℕ → ℕ
| 0 => m
| n + 1 => bit b (shiftLeft' b m n)
