def leaves

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

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

46def leaves(+items: List<&2, J.Lexeme>,
47           -tail: List<J.Token>) -> {forest(J.lex_leaves(items), tail) == flat(items, tail) : List<J.Token>}:
48    match items:
49        case Nil{}: {==}
50        case head <> rest:
51            Equal.cong(List<J.Token>, List<J.Token>, xs => J.decode_lexeme(head) <> xs,
52                forest(J.lex_leaves(rest), tail), flat(rest, tail), leaves(rest, tail))