Search-engine friendly clone of the
ACL2 documentation
.
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
Abnf
Fty-extensions
Isar
Kestrel-utilities
Soft
Bv
Imp-language
Event-macros
C
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
Jimport
Jcinitializer
Jresult
Jstatems+jblocks
Jstatem
Jstatem-case
Jstatemp
Jstatem-for
Make-jstatem-for
Jstatem-for->update
Jstatem-for->test
Jstatem-for->init
Jstatem-for->body
Change-jstatem-for
Jstatem-equiv
Jstatem-ifelse
Jstatem-while
Jstatem-if
Jstatem-do
Jstatem-throw
Jstatem-return
Jstatem-locvar
Jstatem-kind
Jstatem-expr
Jstatem-continue
Jstatem-break
Jstatem-fix
Jstatem-count
Jblock
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
Number-theory
Cryptography
Lists-light
Builtins
Axe
Solidity
Helpers
Std-extensions
Htclient
Typed-lists-light
Arithmetic-light
X86isa
Axe
Execloader
Math
Testing-utilities
Jstatem
Jstatem-for
This is a product type, introduced by
fty::deftagsum
in support of
jstatem
.
Fields
init —
jexpr
test —
jexpr
update —
jexpr
body —
jblock
Subtopics
Make-jstatem-for
Basic constructor macro for
jstatem-for
structures.
Jstatem-for->update
Get the
update
field from a
jstatem-for
.
Jstatem-for->test
Get the
test
field from a
jstatem-for
.
Jstatem-for->init
Get the
init
field from a
jstatem-for
.
Jstatem-for->body
Get the
body
field from a
jstatem-for
.
Change-jstatem-for
Modifying constructor for
jstatem-for
structures.