• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
    • Apt
    • Zfc
    • Acre
    • Milawa
    • Smtlink
    • Abnf
    • Vwsim
    • Isar
    • Wp-gen
    • Dimacs-reader
    • Pfcs
    • Legacy-defrstobj
    • Proof-checker-array
    • Soft
    • C
    • Farray
    • Rp-rewriter
    • Instant-runoff-voting
    • Imp-language
    • Sidekick
    • Leftist-trees
    • Java
      • Atj
        • Atj-implementation
          • Atj-types
          • Atj-java-primitive-array-model
          • Atj-java-abstract-syntax
          • 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
            • Fty-check-mv-let-call
            • Fty-check-if-call
            • Atj-fn-body
            • Atj-string-ascii-java-identifier-p
            • Fty-check-list-call
            • Atj-string-ascii-java-package-name-p
            • Atj-string-ascii-java-identifier-listp
            • *atj-java-lang-class-names*
          • Atj-java-input-types
          • Atj-test-structures
          • Aij-notions
          • Atj-macro-definition
        • Atj-tutorial
      • Aij
      • Language
    • Taspi
    • Bitcoin
    • Riscv
    • Des
    • Ethereum
    • X86isa
    • Sha-2
    • Yul
    • Zcash
    • Proof-checker-itp13
    • Regex
    • ACL2-programming-language
    • Json
    • Jfkr
    • Equational
    • Cryptography
    • Poseidon
    • Where-do-i-place-my-book
    • Axe
    • Bigmems
    • Builtins
    • Execloader
    • Aleo
    • Solidity
    • Paco
    • Concurrent-programs
    • Bls12-377-curves
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Atj-implementation

Atj-library-extensions

Library extensions for atj.

These are used by, but more general than, atj. Thus, they should be moved to more general libraries eventually.

Subtopics

Fty-check-mv-let-call

An FTY variant of check-mv-let-call.

Fty-check-if-call

FTY version of check-if-call.

Atj-fn-body

Return the unnormalized body or attachment of a function.

Atj-string-ascii-java-identifier-p

Check if an ACL2 string is a valid ASCII Java identifier.

Fty-check-list-call

FTY version of check-list-call.

Atj-string-ascii-java-package-name-p

Check if an ACL2 string is a valid ASCII Java package name.

Atj-string-ascii-java-identifier-listp

Check if a list of ACL2 strings includes only ASCII Java identifiers.

*atj-java-lang-class-names*

Class names in the Java java.lang package.