cakeml icon indicating copy to clipboard operation
cakeml copied to clipboard
verified publisher icon CakeML

Move `good_dimindex_def` to a common file

Open hirataqdees opened this issue 4 years ago • 0 comments

good_dimindex is defined in 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 to a common file, lets say miscScript.

hirataqdees avatar Mar 12 '21 21:03 hirataqdees