Standard ML compatibility mode

Open sorear opened this issue 5 years ago • 0 comments

As the compiler improves, we may wish to try to market it to users of SML binary compilers. Currently, CakeML requires its own syntax, which such users generally do not have.

Additionally there would be demo value in being able to run (portions of) HOL4 and the CakeML proof scripts on itself.

This is of limited use without the ability to load code from files (https://github.com/CakeML/cakeml/issues/319#issuecomment-338555569).

Sep 19 '20 13:09 sorear