English
rcons(p) constructs a word by prepending the head-tail pair from p; if the head equals 1, it returns the tail to keep the word reduced.
Русский
rcons(p) строит новое слово, добавляя пару головы и хвоста из p; если голова равна 1, возвращается хвост, чтобы сохранить редуцированность.
LaTeX
$$$ \\mathrm{rcons}\\{i\\} p = \\text{if } p.head = 1 \\text{ then } p.tail else \\mathrm{cons}(p.head, p.tail, p.fstIdx\\_ne, h)$$$
Lean4
/-- Given a pair `(head, tail)`, we can form a word by prepending `head` to `tail`, except if `head`
is `1 : M i` then we have to just return `Word` since we need the result to be reduced. -/
def rcons {i} (p : Pair M i) : Word M :=
if h : p.head = 1 then p.tail else cons p.head p.tail p.fstIdx_ne h
