Def-svtv-data-import
Define a function that imports a particular svtv data object (such as created by def-svtv-data-export) into a svtv-data stobj.
Usage:
(def-svtv-data-import <export-name>)
where <export-name> is the name of a 0-ary function such as produced by
def-svtv-data-export. This creates a function called
svtv-data-import-<export-name> (in the package of <export-name>)
which sets the contents of an svtv-data stobj to those of the export object,
and (crucially) verifies its guards, showing that it preserves the invariant of
the svtv-data stobj.
See also def-svtv-data-export/import which simply combines the export
and import events.
