• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
      • Std/lists
      • Std/alists
      • Obags
      • Std/util
      • Std/strings
      • Std/osets
      • Std/io
      • Std/basic
      • Std/system
        • Fresh-logical-name-with-$s-suffix
        • Irrelevant-formals-info
        • Std/system/function-queries
          • Defun-sk-queries
          • Tail-recursive-p
          • Termination-theorem$
          • Unwrapped-nonexec-body+
          • Measure
          • Arity+
          • Ubody
          • Ruler-extenders+
          • Recursive-calls
          • Guard-theorem-no-simplify$
          • Well-founded-relation+
          • Unwrapped-nonexec-body
          • Measured-subset+
          • Ruler-extenders
          • Measure+
          • Number-of-results+
          • Induction-machine+
          • Non-executablep+
          • Pure-raw-p
          • Irecursivep+
          • Formals+
          • Stobjs-out+
          • Definedp+
          • Number-of-results
          • Induction-machine
          • Ubody+
          • Guard-theorem-no-simplify
          • Uguard
          • Rawp
          • Defchoose-queries
            • Defchoose-body
            • Defchoosep
            • Defchoose-strengthen
              • Defchoose-namep
              • Defchoose-bound-vars
              • Defchoose-untrans-body
            • Uguard+
            • Stobjs-in+
            • No-stobjs-p+
            • Irecursivep
            • Well-founded-relation
            • Definedp
            • Guard-verified-p+
            • Primitivep+
            • No-stobjs-p
            • Measured-subset
            • Guard-verified-p
            • Primitivep
            • Non-executablep
            • Fundef-disabledp
            • Ibody
            • Fundef-enabledp
            • Std/system/arity
          • Std/system/term-queries
          • Std/system/term-transformations
          • Std/system/enhanced-utilities
          • Install-not-normalized-event
          • Install-not-normalized-event-lst
          • Std/system/term-function-recognizers
          • Genvar$
          • Std/system/event-name-queries
          • Pseudo-tests-and-call-listp
          • Maybe-pseudo-event-formp
          • Add-suffix-to-fn-or-const
          • Chk-irrelevant-formals-ok
          • Table-alist+
          • Pseudo-tests-and-callp
          • Add-suffix-to-fn-or-const-lst
          • Known-packages+
          • Add-suffix-to-fn-lst
          • Unquote-term
          • Event-landmark-names
          • Add-suffix-lst
          • Std/system/theorem-queries
          • Unquote-term-list
          • Std/system/macro-queries
          • Pseudo-command-landmark-listp
          • Install-not-normalized$
          • Pseudo-event-landmark-listp
          • Known-packages
          • Std/system/partition-rest-and-keyword-args
          • Rune-enabledp
          • Rune-disabledp
          • Included-books
          • Std/system/pseudo-event-formp
          • Std/system/plist-worldp-with-formals
          • Std/system/w
          • Std/system/geprops
          • Std/system/arglistp
          • Std/system/constant-queries
        • Std/typed-lists
        • Std/bitsets
        • Std/testing
        • Std/typed-alists
        • Std/stobjs
      • Proof-automation
      • Macro-libraries
      • ACL2
      • Interfacing-tools
      • Hardware-verification
      • Software-verification
      • Math
      • Testing-utilities
    • Defchoose-queries

    Defchoose-strengthen

    Value of the :strengthen option of a function introduced via defchoose.

    Signature
    (defchoose-strengthen fn wrld) → t/nil
    Arguments
    fn — Guard (defchoose-namep fn wrld).
    wrld — Guard (plist-worldp wrld).
    Returns
    t/nil — A booleanp.

    If explicitly supplied, the value of the :strengthen option is the last element of the defchoose event, which consists of seven element in this case. If not explicitly supplied, the value of the :strengthen option is nil, and the defchoose event consists of five elements only.

    Definitions and Theorems

    Function: defchoose-strengthen

    (defun defchoose-strengthen (fn wrld)
      (declare (xargs :guard (and (plist-worldp wrld)
                                  (defchoose-namep fn wrld))))
      (let ((__function__ 'defchoose-strengthen))
        (declare (ignorable __function__))
        (let ((event (get-event fn wrld)))
          (if (= (len event) 5)
              nil
            (car (last event))))))