JSONLexWhitespaceProof.lex_scan_context: def of qasim-bend-kit@0.1.0.2
Import: import qasim-bend-kit@0.1.0.2/proof/JSON_LexWhitespaceProof.bend as JSONLexWhitespaceProof
Lines 146-164 of qasim-bend-kit@0.1.0.2/proof/JSON_LexWhitespaceProof.bend: https://jend.leeeet.dev/read.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_LexWhitespaceProof.bend&start_line=146&end_line=164

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

def lex_scan_context(+text: String,
                     +mode1: J.LexMode,
                     +reversed1: String,
                     +acc1: List<&2, J.Lexeme>,
                     +mode2: J.LexMode,
                     +reversed2: String,
                     +acc2: List<&2, J.Lexeme>,
                     mode_eq: {mode1 == mode2 : J.LexMode},
                     reversed_eq: {reversed1 == reversed2 : String},
                     acc_eq: {acc1 == acc2 : List<&2, J.Lexeme>}) -> {J.lex_scan(text, mode1, reversed1, acc1) == J.lex_scan(text, mode2, reversed2, acc2) : List<&2, J.Lexeme>}:
    Equal.trans(List<&2, J.Lexeme>, J.lex_scan(text, mode1, reversed1, acc1),
        J.lex_scan(text, mode2, reversed1, acc1), J.lex_scan(text, mode2, reversed2, acc2),
        Equal.cong(J.LexMode, List<&2, J.Lexeme>, mode => J.lex_scan(text, mode, reversed1, acc1), mode1, mode2, mode_eq),
        Equal.trans(List<&2, J.Lexeme>, J.lex_scan(text, mode2, reversed1, acc1),
            J.lex_scan(text, mode2, reversed2, acc1), J.lex_scan(text, mode2, reversed2, acc2),
            Equal.cong(String, List<&2, J.Lexeme>, reversed => J.lex_scan(text, mode2, reversed, acc1),
                reversed1, reversed2, reversed_eq),
            Equal.cong(List<&2, J.Lexeme>, List<&2, J.Lexeme>, acc => J.lex_scan(text, mode2, reversed2, acc),
                acc1, acc2, acc_eq)))

Uses (7):
  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.trans
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=String
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/JSON.bend&name=LexMode
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/JSON.bend&name=Lexeme
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/JSON.bend&name=lex_scan