• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
    • Std/lists
    • Std/alists
    • Obags
    • Std/util
    • Std/strings
    • Std/io
    • Std/osets
    • Std/basic
    • Std/system
      • Fresh-logical-name-with-$s-suffix
      • Irrelevant-formals-info
      • Std/system/function-queries
        • Defun-sk-queries
          • Defun-sk-matrix
          • Defun-sk-p
          • Defun-sk-namep
          • Defun-sk-body
          • Defun-sk-imatrix
          • Defun-sk-definition-name
          • Defun-sk-witness
          • Defun-sk-classicalp
          • Defun-sk-rewrite-kind
          • Defun-sk-rewrite-name
          • Defun-sk-rewrite-kind-p
          • Defun-sk-quantifier
          • Defun-sk-options
          • Defun-sk-bound-vars
          • Defun-sk-strengthen
          • Defun-sk-quantifier-p
        • 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
        • 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

• Defun-sk-queries

Defun-sk-strengthen

Retrieve the value of the :strengthen option of a function introduced via defun-sk.

Signature

(defun-sk-strengthen fn wrld) → strengthen

Arguments

fn — Guard (defun-sk-namep fn wrld).

wrld — Guard (plist-worldp wrld).

Returns

strengthen — A booleanp.

Definitions and Theorems

Function: defun-sk-strengthen

(defun defun-sk-strengthen (fn wrld)
  (declare (xargs :guard (and (plist-worldp wrld)
                              (defun-sk-namep fn wrld))))
  (let ((__function__ 'defun-sk-strengthen))
    (declare (ignorable __function__))
    (cdr (assoc-eq :strengthen (defun-sk-options fn wrld)))))