Macros that represent Syntheto directly in ACL2.
This is a shallow embedding of Syntheto in ACL2, intended for quick generation of ACL2 definitions from an IDE. This is work in progress.
