Commit 2021-12-23 14:37 91fe0824

feat: @[norm_cast] attribute (#147) I'm not entirely sure I got this right. In particular, I'm not sure if normCastExt should be a builtin_initialize or initialize block. They both seem to work, except that in the initialize version I can't access the environment to construct the initial SimpLemmas object, which is initialized to a nonempty set. As written (but with initialize instead of builtin_initialize), it will crash at the run_cmd line because you can't evaluate an initialize value in the same file as the definition.