PROOF.assemble_source: def of qasim-bend-kit@0.1.0.2
Import: import qasim-bend-kit@0.1.0.2/PROOF.bend as PROOF
Lines 44-69 of qasim-bend-kit@0.1.0.2/PROOF.bend: https://jend.leeeet.dev/read.txt?path=qasim-bend-kit@0.1.0.2/PROOF.bend&start_line=44&end_line=69

import Base
import qasim-bend-kit@0.1.0.2/libs/JSON.bend as Json
import qasim-bend-kit@0.1.0.2/proof/JSON_ParallelProof.bend as ParallelProof
import qasim-bend-kit@0.1.0.2/proof/JSON_AssemblyProof.bend as AssemblyProof
import qasim-bend-kit@0.1.0.2/proof/JSON_SourceProof.bend as SourceProof

def assemble_source(+value: Json.Value) -> {Json.assemble(Json.token_list(Json.decode_tree(Json.lex_tree(Json.source(value, False{}, Nil{}))), Nil{}), Json.NeedValue{Json.Top{}}) == Done{value} : ResultValue()}:
    Equal.trans(ResultValue(),
        Json.assemble(Json.token_list(Json.decode_tree(Json.lex_tree(Json.source(value, False{}, Nil{}))), Nil{}), Json.NeedValue{Json.Top{}}),
        Json.assemble(AssemblyProof.tokens(value, AssemblyProof.Whole{}, Nil{}), AssemblyProof.start(value, AssemblyProof.Whole{}, Nil{}, Nil{}, Json.Top{})),
        Done{value},
        Equal.cong(List<Json.Token>, ResultValue(), tokens => Json.assemble(tokens, Json.NeedValue{Json.Top{}}),
            Json.token_list(Json.decode_tree(Json.lex_tree(Json.source(value, False{}, Nil{}))), Nil{}),
            AssemblyProof.tokens(value, AssemblyProof.Whole{}, Nil{}),
            Equal.trans(List<Json.Token>,
                Json.token_list(Json.decode_tree(Json.lex_tree(Json.source(value, False{}, Nil{}))), Nil{}),
                SourceProof.token_source(Json.source(value, False{}, Nil{}), Nil{}),
                AssemblyProof.tokens(value, AssemblyProof.Whole{}, Nil{}),
                Equal.trans(List<Json.Token>,
                    Json.token_list(Json.decode_tree(Json.lex_tree(Json.source(value, False{}, Nil{}))), Nil{}),
                    ParallelProof.flat(Json.source(value, False{}, Nil{}), Nil{}),
                    SourceProof.token_source(Json.source(value, False{}, Nil{}), Nil{}),
                    ParallelProof.decode(Json.source(value, False{}, Nil{}), Nil{}),
                    Equal.sym(List<Json.Token>, SourceProof.token_source(Json.source(value, False{}, Nil{}), Nil{}),
                        ParallelProof.flat(Json.source(value, False{}, Nil{}), Nil{}),
                        SourceProof.token_source_flat(Json.source(value, False{}, Nil{}), Nil{}))),
                SourceProof.source_tokens(value, AssemblyProof.Whole{}, Nil{}, Nil{}))),
        Equal.trans(ResultValue(),
            Json.assemble(AssemblyProof.tokens(value, AssemblyProof.Whole{}, Nil{}), AssemblyProof.start(value, AssemblyProof.Whole{}, Nil{}, Nil{}, Json.Top{})),
            Json.assemble(Nil{}, Json.assembly_resume(Json.Top{}, value)),
            Done{value},
            AssemblyProof.roundtrip(value, AssemblyProof.Whole{}, Nil{}, Nil{}, Nil{}, Json.Top{}), {==}))

Uses (26):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Result
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/PROOF.bend&name=ResultValue
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/JSON.bend&name=Assembly
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/JSON.bend&name=ParserKont
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/JSON.bend&name=Token
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/JSON.bend&name=Value
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/JSON.bend&name=assemble
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/JSON.bend&name=assembly_resume
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/JSON.bend&name=decode_tree
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/JSON.bend&name=lex_tree
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/JSON.bend&name=source
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/JSON.bend&name=token_list
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_AssemblyProof.bend&name=Mode
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_AssemblyProof.bend&name=roundtrip
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_AssemblyProof.bend&name=start
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_AssemblyProof.bend&name=tokens
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_ParallelProof.bend&name=decode
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_ParallelProof.bend&name=flat
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_SourceProof.bend&name=source_tokens
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_SourceProof.bend&name=token_source
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_SourceProof.bend&name=token_source_flat