• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Community
    • 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
          • Atj
            • Atj-implementation
              • Atj-types
              • Atj-java-primitive-array-model
              • Atj-java-abstract-syntax
                • Jbinop
                • Jmethod
                • Jtype
                • Jfield
                • Jexprs
                • Jliteral
                • Junop
                • Jlocvar
                • Jcunit
                • Jaccess
                • Maybe-jexpr
                • Jparam
                  • Jparam-fix
                  • Jparam-equiv
                  • Make-jparam
                  • Change-jparam
                  • Jparam->type
                  • Jparam->name
                  • Jparam->final?
                  • Jparamp
                • Jimport
                • Jcinitializer
                • Jresult
                • Jstatems+jblocks
                • Jexpr-get-field
                • Jliteral-long-dec-nouscores
                • Nat-to-dec-chars-theorems
                • Jmethods-to-jcbody-elements
                • Jclasses-to-jcbody-elements
                • Jblock-locvar-final
                • Jblock-locvar
                • Jliteral-int-dec-nouscores
                • Jfields-to-jcbody-elements
                • Jblock-for
                • Jblock-smethod
                • Jblock-imethod
                • Jblock-ifelse
                • Jblock-asg-name
                • Jparam-list->types
                • Jparam-list->names
                • Jexpr-lit-long-dec-nouscores
                • Jexpr-lit-int-dec-nouscores
                • Jexpr-literal-string
                • Jexpr-literal-floating
                • Jexpr-literal-character
                • Jblock-while
                • Jblock-method
                • Jblock-if
                • Jblock-expr
                • Jblock-do
                • Jblock-asg
                • Jexpr-name-list
                • Jblock-throw
                • Jblock-return
                • Jparam-list
                • Jimport-list
                • Jexpr-literal-true
                • Jexpr-literal-null
                • Jexpr-literal-false
                • Jexpr-literal-1
                • Jexpr-literal-0
                • Jclass-list
                • Jblock-continue
                • Jtype-short
                • Jtype-long
                • Jtype-list
                • Jtype-int
                • Jtype-float
                • Jtype-double
                • Jtype-char
                • Jtype-byte
                • Jtype-boolean
                • Jmethod-list
                • Jliteral-list
                • Jfield-list
                • Jblock-list
                • Jblock-break
                • Jclasses+jcmembers
              • Atj-input-processing
              • Atj-java-pretty-printer
              • Atj-code-generation
              • Atj-java-primitives
              • Atj-java-primitive-arrays
              • Atj-type-macros
              • Atj-java-syntax-operations
              • Atj-fn
              • Atj-library-extensions
              • Atj-java-input-types
              • Atj-test-structures
              • Aij-notions
              • Atj-macro-definition
            • Atj-tutorial
          • Aij
          • Language
        • Bitcoin
        • Ethereum
        • Yul
        • 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
  • Atj-java-abstract-syntax

Jparam

Java formal parameter [JLS14:8.4.1].

This is a product type introduced by fty::defprod.

Fields
final? — booleanp
type — jtype
name — stringp

We do not capture variable arity parameters.

We only capture parameters without array square brackets after the name (i.e. all the array square brackets are in the type).

Subtopics

Jparam-fix
Fixing function for jparam structures.
Jparam-equiv
Basic equivalence relation for jparam structures.
Make-jparam
Basic constructor macro for jparam structures.
Change-jparam
Modifying constructor for jparam structures.
Jparam->type
Get the type field from a jparam.
Jparam->name
Get the name field from a jparam.
Jparam->final?
Get the final? field from a jparam.
Jparamp
Recognizer for jparam structures.