• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
      • Theories
      • Rule-classes
        • Type-prescription
        • Rewrite
        • Meta
          • Force
          • Syntaxp
          • Extended-metafunctions
          • Meta-extract
          • Backchain-limit
          • Magic-ev-fncall
          • Evaluator-restrictions
          • Meta-implicit-hypothesis
          • Transparent-functions
          • Set-skip-meta-termp-checks
          • Case-split
          • Term-table
          • Magic-ev
          • Meta-lemmas
            • Meta-functions
              • Expand-member-meta
              • Reduce-nth-meta
              • Beta-reduce
              • Formal-member
              • Formal-true-listp
              • Formal-consp
                • Formal-nth
              • Meta-lemma-theory
            • Set-skip-meta-termp-checks!
          • Linear
          • Definition
          • Clause-processor
          • Tau-system
          • Forward-chaining
          • Equivalence
          • Congruence
          • Free-variables
          • Executable-counterpart
          • Induction
          • Type-reasoning
          • Compound-recognizer
          • Rewrite-quoted-constant
          • Elim
          • Well-founded-relation-rule
          • Built-in-clause
          • Well-formedness-guarantee
          • Patterned-congruence
          • Rule-classes-introduction
          • Guard-holders
          • Refinement
          • Type-set-inverter
          • Generalize
          • Corollary
          • Induction-heuristics
          • Backchaining
          • Default-backchain-limit
        • Proof-builder
        • Recursion-and-induction
        • Hons-and-memoization
        • Events
        • Parallelism
        • History
        • Programming
        • Operational-semantics
        • Real
        • Start-here
        • Debugging
        • Miscellaneous
        • Output-controls
        • Macros
        • Interfacing-tools
      • Interfacing-tools
      • Hardware-verification
      • Software-verification
      • Math
      • Testing-utilities
    • Meta-functions

    Formal-consp

    The definition of consp on formal terms.

    Note that FORMAL-CONSP is a `formal' predicate returning (QUOTE T) or (QUOTE NIL).

    Definitions and Theorems

    Function: formal-consp

    (defun formal-consp (term)
  (declare (xargs :guard (pseudo-termp term)))
  (case-match term
    (('quote x)
     (cons 'quote (cons (consp x) 'nil)))
    (('cons x y) (declare (ignore x y)) *t*)
    (& *nil*)))