myreen

Consistently follow pureLang's example of pure_exp_lemmas, pure_eval_lemmas. For backend languages these should be in compiler/backend/languages/properties.

Currently, ThunkLang's definition of `cexp_wf`, `exp_of` etc. are in the wrong places considering the conventions that EnvLang and StateLang follow. This issue is about adjusting files so that ThunkLang follows...

In emacs, `End` is highlighted as a keyword but `Quote` is not. ``` Quote cakeml: fun print_list ls = case ls of [] => () | (x::xs) => (print x;...

Consider adding support for [these SML operations](https://smlfamily.github.io/Basis/int-inf.html) to CakeML. The CakeML semantics for these operations can probably be based on [these definitions from HOL](https://github.com/HOL-Theorem-Prover/HOL/blob/develop/src/integer/int_bitwiseScript.sml). With these implemented in CakeML, one...

@tanyongkiam noticed that cutsets are sometimes too large. For example, the explorer output reveals: ``` (seq ... (6 := Mult (5 4) (some {4,5})) (return 6)) ``` Here 4 and...