• 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
        • Syntax-for-tools
        • Atc
          • Atc-implementation
            • Atc-abstract-syntax
            • Atc-pretty-printer
            • Atc-event-and-code-generation
            • Fty-pseudo-term-utilities
            • Atc-term-recognizers
            • Atc-input-processing
              • Atc-process-target
              • Atc-process-const-name
              • Atc-process-function
              • Atc-process-target-list
              • Atc-process-inputs
              • Atc-process-file-name
              • Atc-process-const-name-aux
              • Atc-process-targets
              • Atc-process-print
              • Atc-process-pretty-printing
              • Atc-remove-called-fns
              • Atc-process-output-dir
              • Atc-process-proofs
              • Atc-process-header
              • *atc-allowed-pretty-printing-options*
              • *atc-allowed-options*
            • Atc-shallow-embedding
            • Atc-process-inputs-and-gen-everything
            • Atc-table
            • Atc-fn
            • Atc-pretty-printing-options
            • Atc-types
            • Atc-macro-definition
          • Atc-tutorial
        • Language
        • Representation
        • Transformation-tools
        • Insertion-sort
        • Pack
      • Farray
      • Rp-rewriter
      • Instant-runoff-voting
      • Imp-language
      • Sidekick
      • Leftist-trees
      • Java
      • 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
  • Atc-implementation

Atc-input-processing

Input processing performed by atc.

See input processing for general background.

Subtopics

Atc-process-target
Process a target among t1, ..., tp.
Atc-process-const-name
Process the :const-name input.
Atc-process-function
Process a target function fn among t1, ..., tp.
Atc-process-target-list
Lift atc-process-function to lists.
Atc-process-inputs
Process all the inputs.
Atc-process-file-name
Process the :file-name input.
Atc-process-const-name-aux
Atc-process-targets
Process the targets t1, ..., tp.
Atc-process-print
Process the :print input.
Atc-process-pretty-printing
Process the :pretty-printing input.
Atc-remove-called-fns
Remove from a list of function symbols all the functions called by a term.
Atc-process-output-dir
Process the :output-dir input.
Atc-process-proofs
Process the :proofs input.
Atc-process-header
Process the :header input.
*atc-allowed-pretty-printing-options*
Keyword (sub)options accepted by atc for the :pretty-printing option.
*atc-allowed-options*
Keyword options accepted by atc.