|
|
|---|
|
|
|
|---|
Translation between Syntheto and ACL2.
Since Syntheto is a front-end language for ACL2 (and APT), there is a mapping between the two. We are developing a bidirectional translation between the two.
The translation is more than turning constructs in one language into corresponding constructs of the other language. In particular, when translating Syntheto to ACL2, we also need to submit and keep track of the ACL2 events corresponding to the Syntheto constructs.