def token_source_flat

qasim-bend-kit@0.1.0.2 · proof/JSON_SourceProof.bend:16

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

16def token_source_flat(+xs: List<&2, J.Lexeme>,
17                      -tail: List<J.Token>) -> {token_source(xs, tail) == Par.flat(xs, tail) : List<J.Token>}:
18    match xs:
19        case Nil{}: {==}
20        case head <> rest:
21            Equal.cong(List<J.Token>, List<J.Token>, tokens => J.decode_lexeme(head) <> tokens,
22                token_source(rest, tail), Par.flat(rest, tail), token_source_flat(rest, tail))