def join

qasim-bend-kit@0.1.0.2 · proof/JSON_ParallelProof.bend:15

import Base
import qasim-bend-kit@0.1.0.2/libs/JSON.bend as J

15def join(+trees: List<&2, J.LexTree>,
16         -tail: List<J.Token>) -> {J.token_list(J.decode_tree(J.lex_join(trees)), tail) == forest(trees, tail) : List<J.Token>}:
17    match trees:
18        case Nil{}: {==}
19        case head <> rest:
20            Equal.cong(List<J.Token>, List<J.Token>, xs => J.token_list(J.decode_tree(head), xs),
21                J.token_list(J.decode_tree(J.lex_join(rest)), tail), forest(rest, tail), join(rest, tail))