def append_nil_r

mylsm-lsm-store@0.3.2.0 · src/Wal.bend:263

import Base

263def append_nil_r(+xs: List<&2, Mut>) -> {List.append(&2, Mut, xs, Nil{}) == xs : List<&2, Mut>}:
264  match xs:
265    case Nil{}:
266      {==}
267    case Con{h, t}:
268      %append_nil_r(t) : {Con{h, List.append(&2, Mut, t, Nil{})} == Con{h, _} : List<&2, Mut>}
269      {==}