• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Community
    • Proof-automation
    • Macro-libraries
    • ACL2
      • Theories
      • Rule-classes
      • Proof-builder
      • Recursion-and-induction
      • Hons-and-memoization
      • Events
      • Parallelism
      • History
      • Programming
      • Operational-semantics
      • Real
      • Start-here
      • Debugging
      • Miscellaneous
        • Term
          • Lambda
          • Pseudo-termp
            • Pseudo-term-fty
              • Pseudo-term-lambda
              • Pseudo-term-call
                • Pseudo-term-call->fn
                  • Pseudo-term-call->args
                • Pseudo-term-fncall
                • Pseudo-lambda
                • Pseudo-term-var
                • Pseudo-term-quote
                • Pseudo-term-kind
                • Pseudo-term-null
                • Pseudo-fnsym
                • Pseudo-term-case
                • Pseudo-term-count
                • Def-ev-pseudo-term-fty-support
                • Def-ev-pseudo-term-congruence
                • Pseudo-term-fix
                • Pseudo-var
                • Pseudo-term-list-fix
                • Pseudo-fn
              • Std/typed-lists/pseudo-term-listp
            • Term-order
            • Pseudo-term-listp
            • Guard-holders
            • Termp
            • Termify
            • L<
            • Kwote
            • Kwote-lst
          • Ld
          • Hints
          • Type-set
          • Ordinals
          • Clause
          • ACL2-customization
          • With-prover-step-limit
          • Set-prover-step-limit
          • With-prover-time-limit
          • Local-incompatibility
          • Set-case-split-limitations
          • Subversive-recursions
          • Specious-simplification
          • Defsum
          • Gcl
          • Oracle-timelimit
          • Thm
          • Defopener
          • Case-split-limitations
          • Set-gc-strategy
          • Default-defun-mode
          • Top-level
          • Reader
          • Divp-by-casting
          • Ttags-seen
          • Adviser
          • Ttree
          • Abort-soft
          • Defsums
          • Gc$
          • With-timeout
          • Coi-debug::fail
          • Expander
          • Gc-strategy
          • Coi-debug::assert
          • Sin-cos
          • Majority-vote
          • Def::doc
          • Syntax
          • Subversive-inductions
        • Output-controls
        • Macros
        • Interfacing-tools
      • Interfacing-tools
      • Hardware-verification
      • Software-verification
      • Math
      • Testing-utilities
    • Pseudo-term-call
    • Pseudo-term-fncall
    • Pseudo-term-lambda

    Pseudo-term-call->fn

    Accessor for the function of a function call or lambda call pseduo-term.

    Signature
    (pseudo-term-call->fn x) → fn
    Arguments
    x — Guard (pseudo-termp x).
    Returns
    fn — Type (pseudo-fn-p fn).

    Definitions and Theorems

    Function: pseudo-term-call->fn

    (defun pseudo-term-call->fn (x)
      (declare (xargs :guard (pseudo-termp x)))
      (declare (xargs :guard (member-eq (pseudo-term-kind x)
                                        '(:fncall :lambda))))
      (let ((__function__ 'pseudo-term-call->fn))
        (declare (ignorable __function__))
        (mbe :logic (and (or (eq (pseudo-term-kind x) :lambda)
                             (eq (pseudo-term-kind x) :fncall))
                         (car (pseudo-term-fix x)))
             :exec (car x))))

    Theorem: pseudo-fn-p-of-pseudo-term-call->fn

    (defthm pseudo-fn-p-of-pseudo-term-call->fn
      (b* ((fn (pseudo-term-call->fn x)))
        (pseudo-fn-p fn))
      :rule-classes :rewrite)

    Theorem: not-quote-of-pseudo-term-call->fn

    (defthm not-quote-of-pseudo-term-call->fn
      (not (equal (pseudo-term-call->fn x)
                  'quote)))

    Theorem: pseudo-term-call->fn-when-lambda

    (defthm pseudo-term-call->fn-when-lambda
      (implies (eq (pseudo-term-kind x) :lambda)
               (equal (pseudo-term-call->fn x)
                      (pseudo-term-lambda->fn x))))

    Theorem: pseudo-term-call->fn-when-fncall

    (defthm pseudo-term-call->fn-when-fncall
      (implies (eq (pseudo-term-kind x) :fncall)
               (equal (pseudo-term-call->fn x)
                      (pseudo-term-fncall->fn x))))

    Theorem: pseudo-term-call->fn-of-pseudo-term-fix-x

    (defthm pseudo-term-call->fn-of-pseudo-term-fix-x
      (equal (pseudo-term-call->fn (pseudo-term-fix x))
             (pseudo-term-call->fn x)))

    Theorem: pseudo-term-call->fn-pseudo-term-equiv-congruence-on-x

    (defthm pseudo-term-call->fn-pseudo-term-equiv-congruence-on-x
      (implies (pseudo-term-equiv x x-equiv)
               (equal (pseudo-term-call->fn x)
                      (pseudo-term-call->fn x-equiv)))
      :rule-classes :congruence)