hirataqdees issues

Repositories
Issues
Comments

Results 1 issues of


                                            hirataqdees

Move `good_dimindex_def` to a common file

`good_dimindex` is defined in [labPropsScript.sml](https://github.com/CakeML/cakeml/blob/master/compiler/backend/semantics/labPropsScript.sml). This makes its usage elsewhere dependent on `labPropsTheory` and hence also the frontend files. It would be best to move the definition and related theorems...

enhancement