• 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
          • Atj
            • Atj-implementation
              • Atj-types
              • Atj-java-primitive-array-model
              • Atj-java-abstract-syntax
                • Jbinop
                • Jmethod
                • Jtype
                • Jfield
                • Jexprs
                • Jliteral
                • Junop
                • Jlocvar
                  • Jlocvar-fix
                  • Make-jlocvar
                  • Jlocvar-equiv
                  • Change-jlocvar
                  • Jlocvar->name
                  • Jlocvar->init?
                  • Jlocvar->final?
                  • Jlocvar->type
                  • Jlocvarp
                • Jcunit
                • Jaccess
                • Maybe-jexpr
                • Jparam
                • 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

Jlocvar

Local variable declarations [JLS14:14.4].

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

Fields
final? — booleanp
type — jtype
name — stringp
init? — maybe-jexpr

We only capture declarations of single local variables without array square brackets after the name (i.e. all the array square brackets are in the type). The declarations have an optional initializer.

We do not capture var.

Subtopics

Jlocvar-fix
Fixing function for jlocvar structures.
Make-jlocvar
Basic constructor macro for jlocvar structures.
Jlocvar-equiv
Basic equivalence relation for jlocvar structures.
Change-jlocvar
Modifying constructor for jlocvar structures.
Jlocvar->name
Get the name field from a jlocvar.
Jlocvar->init?
Get the init? field from a jlocvar.
Jlocvar->final?
Get the final? field from a jlocvar.
Jlocvar->type
Get the type field from a jlocvar.
Jlocvarp
Recognizer for jlocvar structures.