Macro to lift a deeply embedded PFCS definition to a shallowly embedded PFCS definition with a theorem relating the two.
The required argument must be a ground form that evaluates to a PFCS definition. The form is evaluated and the resulting definition is processed.
The keyword argument must be a symbol
to use for the prime that parameterizes the PFCS semantics.
It is
Macro:
(defmacro lift (def &key (prime 'p)) (cons 'make-event (cons (cons 'lift-fn (cons def (cons (cons 'quote (cons prime 'nil)) '(state)))) 'nil)))