• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
      • Apt
      • Acre
      • Milawa
      • Smtlink
      • Aleobft
      • Abnf
      • Vwsim
      • Isar
      • Wp-gen
      • Dimacs-reader
      • Pfcs
        • Proof-support
        • Abstract-syntax
        • R1cs-subset
        • Semantics
        • Abstract-syntax-operations
        • Indexed-names
        • Well-formedness
        • Concrete-syntax
          • Lexer
          • Grammar
          • Parser
            • Parse-separator
            • Parse-operator
            • Parse-definition
            • Parse-relation-constraint
            • Parse-equality-constraint
            • Parse-*-comma-identifier
            • Parse-*-comma-expression
            • Parse-*-comma-constraint
            • Parse-system
            • Parse-identifier
            • Parse-pfcs-integer
            • Parse-constraint
            • Parse-*-definition
            • Parse-*-constraint
            • Parsize
            • Check-token-string
            • Check-token-root
            • Parse-token
            • Token-stringp
            • Token-rootp
            • Patbind-pok<
            • Parse-multiplication-expression-rest
            • Parse-addition-expression-rest
            • Parse-primary-expression
              • Parse-multiplication-expression
              • Parse-addition-expression
              • Parse-expression
              • Patbind-pok
              • Perr
            • Abnf-extensions
            • Tokenizer
          • R1cs-bridge
          • Parser-interface
        • Legacy-defrstobj
        • Proof-checker-array
        • Soft
        • Farray
        • Rp-rewriter
        • Instant-runoff-voting
        • Imp-language
        • Sidekick
        • Leftist-trees
        • C
        • Java
        • Taspi
        • Bitcoin
        • Des
        • Ethereum
        • X86isa
        • Sha-2
        • Riscv
        • Yul
        • Zcash
        • Proof-checker-itp13
        • Regex
        • ACL2-programming-language
        • Json
        • Jfkr
        • Equational
        • Cryptography
        • Poseidon
        • Where-do-i-place-my-book
        • Bigmems
        • Builtins
        • Axe
        • Execloader
        • Solidity
        • Leo
        • Paco
        • Concurrent-programs
      • Debugging
      • Std
      • Proof-automation
      • Macro-libraries
      • ACL2
      • Interfacing-tools
      • Hardware-verification
      • Software-verification
      • Math
      • Testing-utilities
    • Parser

    Parse-primary-expression

    Parse a primary-expression.

    Signature
    (parse-primary-expression token input) 
  → 
(mv tree next-token rest-input)
    Arguments
    token — Guard (abnf::tree-optionp token).
    input — Guard (abnf::tree-listp input).
    Returns
    tree — Type (abnf::tree-resultp tree).
    next-token — Type (abnf::tree-optionp next-token).
    rest-input — Type (abnf::tree-listp rest-input).