def lex_scan_step

qasim-bend-kit@0.1.0.2 · proof/JSON_LexWhitespaceProof.bend:61

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

61def lex_scan_step(+head: Char,
62                  +tail: String,
63                  +mode: J.LexMode,
64                  +reversed: String,
65                  +acc: List<&2, J.Lexeme>) -> {J.lex_scan(SCon{head, tail}, mode, reversed, acc) == J.lex_scan(tail, after_mode(J.lex_seed_action(SCon{head, tail}, mode), mode), after_reversed(J.lex_seed_action(SCon{head, tail}, mode), head, reversed), after_acc(J.lex_seed_action(SCon{head, tail}, mode), head, reversed, acc)) : List<&2, J.Lexeme>}:
66    Equal.trans(List<&2, J.Lexeme>, J.lex_scan(SCon{head, tail}, mode, reversed, acc),
67        J.lexemes(SCon{head, tail}, mode, reversed, acc, J.lex_seed_action(SCon{head, tail}, mode)),
68        J.lex_scan(tail, after_mode(J.lex_seed_action(SCon{head, tail}, mode), mode),
69            after_reversed(J.lex_seed_action(SCon{head, tail}, mode), head, reversed),
70            after_acc(J.lex_seed_action(SCon{head, tail}, mode), head, reversed, acc)),
71        {==}, lexemes_step(head, tail, mode, reversed, acc, J.lex_seed_action(SCon{head, tail}, mode)))