|
|
|---|
|
|
|
|---|
Well-founded relation of a named logic-mode recursive function.
(well-founded-relation fn wrld) → well-founded-relation
See well-founded-relation-rule
for a discussion of well-founded relations in ACL2,
including the
See well-founded-relation+ for an enhanced variant of this utility.
Function:
(defun well-founded-relation (fn wrld) (declare (xargs :guard (and (symbolp fn) (plist-worldp wrld)))) (let ((__function__ 'well-founded-relation)) (declare (ignorable __function__)) (b* ((justification (getpropc fn 'justification nil wrld))) (access justification justification :rel))))