Move good_dimindex_def to a common file
#818
Labels
Comments
IlmariReissumies
added a commit
that referenced
this issue
Mar 14, 2023
good_dimindex is needed here and there. It seems silly to pollute the dependency graph with imports of labProps just for that. Fixes issue #818.
mktnk3
pushed a commit
to mktnk3/cakeml
that referenced
this issue
May 10, 2023
good_dimindex is needed here and there. It seems silly to pollute the dependency graph with imports of labProps just for that. Fixes issue CakeML#818.
mktnk3
pushed a commit
that referenced
this issue
May 10, 2023
good_dimindex is needed here and there. It seems silly to pollute the dependency graph with imports of labProps just for that. Fixes issue #818.
xdrr
pushed a commit
to xdrr/cakeml
that referenced
this issue
Jul 8, 2023
good_dimindex is needed here and there. It seems silly to pollute the dependency graph with imports of labProps just for that. Fixes issue CakeML#818.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
good_dimindexis defined in labPropsScript.sml. This makes its usage elsewhere dependent onlabPropsTheoryand hence also the frontend files. It would be best to move the definition and related theorems to a common file, lets say miscScript.The text was updated successfully, but these errors were encountered: