def app_assoc

bend-osdev-acpi@0.1.1.0 · PROOF.bend:1983

import Base
import bend-osdev-bytes@0.1.1.0/bytes.bend as B

1983def app_assoc(+a: List<&2, U32>, +b: List<&2, U32>, +c: List<&2, U32>) -> {B.append(a, B.append(b, c)) == B.append(B.append(a, b), c) : List<&2, U32>}:
1984  match a:
1985    case Nil{}:
1986      {==}
1987    case Con{h, t}:
1988      %app_assoc(t, b, c) : {Con{h, B.append(t, B.append(b, c))} == Con{h, _} : List<&2, U32>}
1989      {==}