• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
      • Apt
      • Zfc
      • Acre
      • Milawa
      • Smtlink
      • Abnf
      • Vwsim
      • Isar
      • Wp-gen
      • Dimacs-reader
      • Pfcs
      • Legacy-defrstobj
      • Proof-checker-array
      • Soft
      • C
      • Farray
      • Rp-rewriter
      • Instant-runoff-voting
      • Imp-language
      • Sidekick
      • Leftist-trees
      • Java
      • Taspi
      • Bitcoin
      • Riscv
      • Des
      • Ethereum
      • X86isa
      • Sha-2
      • Yul
        • Transformations
        • Language
          • Abstract-syntax
          • Dynamic-semantics
          • Concrete-syntax
            • Lexer
            • Parser
              • Parse-keyword
              • Parse-variable-declaration
              • Parse-symbol
              • Parse-literal
              • Parse-identifier
              • Hex-chars-and-uscores-to-hex-string-rest-element-list
              • Parse-assignment-statement
              • Parse-identifier-and-open-paren
              • Parse-*-comma-identifier
              • Parse-*-.-identifier
              • Parse-continue-statement
              • Parse-*-comma-path
              • Parse-path
              • Parse-leave-statement
              • Parse-break-statement
              • Cst2ast-hex-string
              • Cst2ast-string-literal-content
              • Cst2ast-escape-sequence
              • Cst2ast-string-literal-contents
              • Cst2ast-quoted-printable
              • Parse-yul
              • Cst2ast-string-literal
              • Parse-yul-bytes
              • Cst2ast-hex-number
              • Cst2ast-uhhhh
              • Cst2ast-literal-kind
              • Cst2ast-decimal-number
              • Cst2ast-xhh
              • Cst2ast-single-char
              • Cst2ast-boolean
              • Parse-*-case-clause
              • Looks-like-hex-string-fringe
              • Cst2ast-hex-digit-char-list
              • Parse-*-statement
              • Parse-*-comma-expression
              • Parse-switch-statement
                • Parse-if-statement
                • Parse-for-statement
                • Parse-expression
                • Parse-case-clause
                • Parse-fundef
                • Parse-function-call
                • Parse-block
                • *single-quote-tree-list*
                • *double-quote-tree-list*
                • *yul-keywords*
                • *single-quoted-content-rulenames*
                • *list-leafterm-x*
                • *list-leafterm-u*
                • *list-leafterm-92*
                • *double-quoted-content-rulenames*
                • *yul-symbols*
              • Grammar-old
              • Grammar
              • Tokenizer
            • Static-soundness
            • Static-semantics
            • Errors
          • Yul-json
        • Zcash
        • Proof-checker-itp13
        • Regex
        • ACL2-programming-language
        • Json
        • Jfkr
        • Equational
        • Cryptography
        • Poseidon
        • Where-do-i-place-my-book
        • Axe
        • Bigmems
        • Builtins
        • Execloader
        • Aleo
        • Solidity
        • Paco
        • Concurrent-programs
        • Bls12-377-curves
      • Debugging
      • Std
      • Proof-automation
      • Macro-libraries
      • ACL2
      • Interfacing-tools
      • Hardware-verification
      • Software-verification
      • Math
      • Testing-utilities
    • Parser

    Parse-switch-statement

    Eats a switch statement and builds a statement AST node of kind :switch.

    Signature
    (parse-switch-statement tokens) 
      → 
    (mv result-ast tokens-after-statement)
    Arguments
    tokens — Guard (abnf::tree-listp tokens).
    Returns
    result-ast — Type (statement-resultp result-ast).
    tokens-after-statement — Type (abnf::tree-listp tokens-after-statement).