• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
      • Kestrel-books
        • Crypto-hdwallet
        • Apt
        • Error-checking
        • Fty-extensions
        • Isar
        • Kestrel-utilities
        • Set
        • Soft
        • C
        • Bv
        • Imp-language
        • Event-macros
        • Java
        • Bitcoin
        • Ethereum
        • 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
          • ACL2-programming-language
          • Prime-fields
          • Json
          • Syntheto
          • File-io-light
          • Cryptography
          • Number-theory
          • Lists-light
          • Axe
          • Builtins
          • Solidity
          • Helpers
          • Htclient
          • Typed-lists-light
          • Arithmetic-light
        • X86isa
        • Axe
        • Execloader
      • Math
      • Testing-utilities
    • Parser

    Parse-expression

    Attempts to eat an expression and build an expression AST node.

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