def reverse_go_append

qasim-bend-kit@0.1.0.2 · proof/JSON_ListProof.bend:27

import Base

27def reverse_go_append(-A: Data,
28                      +xs: List<&2, A>,
29                      +acc: List<&2, A>,
30                      +tail: List<&2, A>) -> {List.reverse.go(&2, A, xs, List.append(&2, A, acc, tail)) == List.append(&2, A, List.reverse.go(&2, A, xs, acc), tail) : List<&2, A>}:
31    match xs:
32        case Nil{}: {==}
33        case h <> t:
34            reverse_go_append(A, t, h <> acc, tail)