def lex_source

qasim-bend-kit@0.1.0.2 · proof/JSON_RenderLexProof.bend:551

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_SourceProof.bend as SP
import qasim-bend-kit@0.1.0.2/proof/JSON_ListProof.bend as LP

551def lex_source(+value: J.Value) -> {J.lex_scan(J.stringify(value), J.Outside{}, SNil{}, Nil{}) == J.source(value, False{}, Nil{}) : List<&2, J.Lexeme>}:
552    Equal.trans(List<&2, J.Lexeme>,
553        J.lex_scan(J.stringify(value), J.Outside{}, SNil{}, Nil{}),
554        finish(End{}, push(value, SP.RenderWhole{}, Nil{})),
555        J.source(value, False{}, Nil{}),
556        lex_value(value, SP.RenderWhole{}, End{}, Nil{}),
557        LP.reverse_twice(J.Lexeme, J.source(value, False{}, Nil{})))