		Search-engine friendly clone of the ACL2 documentation.

Expdata-surjmapp

Make-honsed-expdata-surjmap

Constructor macro for honsed expdata-surjmapp structures.

Syntax:

(make-honsed-expdata-surjmap [:surjname <surjname>] 
                             [:localp <localp>] 
                             [:oldp <oldp>] 
                             [:newp <newp>] 
                             [:forth <forth>] 
                             [:back <back>] 
                             [:forth-image <forth-image>] 
                             [:back-image <back-image>] 
                             [:back-of-forth <back-of-forth>] 
                             [:forth-injective <forth-injective>] 
                             [:oldp-guard <oldp-guard>] 
                             [:newp-guard <newp-guard>] 
                             [:forth-guard <forth-guard>] 
                             [:back-guard <back-guard>] 
                             [:hints <hints>])

This is identical to make-expdata-surjmap, except that we hons the structure we are creating.

Definition

This is an ordinary honsing make- macro introduced by std::defaggregate.

Macro: make-honsed-expdata-surjmap

(defmacro make-honsed-expdata-surjmap (&rest args)
  (std::make-aggregate 'expdata-surjmap
                       args
                       '((:surjname)
                         (:localp)
                         (:oldp)
                         (:newp)
                         (:forth)
                         (:back)
                         (:forth-image)
                         (:back-image)
                         (:back-of-forth)
                         (:forth-injective)
                         (:oldp-guard)
                         (:newp-guard)
                         (:forth-guard)
                         (:back-guard)
                         (:hints))
                       'make-honsed-expdata-surjmap
                       t))