|
|
|---|
|
|
|
|---|
Translate to ACL2 a Syntheto top-level construct or a list of them.
This is the entry point of the translation from Syntheto to ACL2. The argument is evaluated, and it must evaluate to a Syntheto top-level construct or to a list of them; this is checked by the function called by this macro. The function returns events that are submitted to ACL2 by this macro. The events update the translation state table and generate ACL2 counterparts of the Syntheto construct(s).
Macro:
(defmacro translate-to-acl2 (top/tops) (cons 'make-event (cons (cons 'translate-to-acl2-fn (cons top/tops '('translate-to-acl2 state))) 'nil)))