|
|
|---|
|
|
|
|---|
Raw constructor for honsed defdigits-infop structures.
Syntax:
(honsed-defdigits-info base digit-pred digit-fix
digits-pred digits-fix bendian-to-nat
lendian-to-nat nat-to-bendian
nat-to-lendian digits-description
digit-pred-correct digit-fix-correct
digits-pred-correct digits-fix-correct)This is identical to defdigits-info, except that we hons the structure we are creating.
This is an ordinary honsing constructor introduced by std::defaggregate.
Function:
(defun honsed-defdigits-info (base digit-pred digit-fix digits-pred digits-fix bendian-to-nat lendian-to-nat nat-to-bendian nat-to-lendian digits-description digit-pred-correct digit-fix-correct digits-pred-correct digits-fix-correct) (declare (xargs :guard (and (dab-basep base) (symbolp digit-pred) (symbolp digit-fix) (symbolp digits-pred) (symbolp digits-fix) (symbolp bendian-to-nat) (symbolp lendian-to-nat) (symbolp nat-to-bendian) (symbolp nat-to-lendian) (stringp digits-description) (symbolp digit-pred-correct) (symbolp digit-fix-correct) (symbolp digits-pred-correct) (symbolp digits-fix-correct)))) (mbe :logic (defdigits-info base digit-pred digit-fix digits-pred digits-fix bendian-to-nat lendian-to-nat nat-to-bendian nat-to-lendian digits-description digit-pred-correct digit-fix-correct digits-pred-correct digits-fix-correct) :exec (hons (hons 'base base) (hons (hons 'digit-pred digit-pred) (hons (hons 'digit-fix digit-fix) (hons (hons 'digits-pred digits-pred) (hons (hons 'digits-fix digits-fix) (hons (hons 'bendian-to-nat bendian-to-nat) (hons (hons 'lendian-to-nat lendian-to-nat) (hons (hons 'nat-to-bendian nat-to-bendian) (hons (hons 'nat-to-lendian nat-to-lendian) (hons (hons 'digits-description digits-description) (hons (hons 'digit-pred-correct digit-pred-correct) (hons (hons 'digit-fix-correct digit-fix-correct) (hons (hons 'digits-pred-correct digits-pred-correct) (hons (hons 'digits-fix-correct digits-fix-correct) nil))))))))))))))))