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;...

Add support for bitwise operations over ints to CakeML

1

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...

Make cutsets smaller in DataLang

1

@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...

Local theorems don't show up in search results

1

``` Theorem foo[local]: 1 + 2 + 3 = 6:num Proof fs [] QED (* the following don't print anything *) print_match [] “_ = 6:num”; print_find "foo"; ```

Support definitions that are local to a theory

3

I would like to be able to write `local` on some definitions: ``` Definition foo_def[local]: foo n = n + 1:num End ``` The intended meaning is the same as...

Add simple form of higher-order inlining

1

I suspect CakeML would do better on a number of benchmarks and real-world examples if we optimised `tabulate`, `map`, `filter`, `genlist`, `every` etc. for cases where they take a known...