Move array stuff to own file

#245 (closed) talks about IntoAnd, but I mirrored what we got for big_sepL and that's IntoSep. However, I also remembered why we didn't do that for lambdaRust: there, array-mapsto is fractional, and then there is the question whether one wants to split at the fraction or the list. We decided that the proofmode would split at the fraction. If we agree that's the more reasonable choice, we should not add the splitting-at-the-list now because then we couldn't extend array-mapsto to fractions later.

However, I also remembered why we didn't do that for lambdaRust: there, array-mapsto is fractional, and then there is the question whether one wants to split at the fraction or the list. We decided that the proofmode would split at the fraction. If we agree that's the more reasonable choice, we should not add the splitting-at-the-list now because then we couldn't extend array-mapsto to fractions late

If we want to make array fractional, then we have overlapping instances and thus a problem.

Although I think that splitting at the list is more useful, I would say that splitting at the fraction would be more consistent. So, I'm probably in favor of the latter.

More consistent with what? I am not convinced that consistency with lambda-Rust should weigh heavily here.

But it is indeed otherwise the case that everything fractional is by default split at the fraction.

More consistent with the fact that everything fractional is by default split at the fraction.

changed milestone to %Iris 3.2

added 1 commit

• b66b4113 - prepare for having fractional arrays in the future

Compare with previous version

added 1 commit

• 9e8004f8 - prepare for having fractional arrays in the future

Compare with previous version

I updated the MR to prepare for a fractional future. But that means there are not actually any new instances.

changed title from Move array stuff to own file and add ProofMode instances to Move array stuff to own file

changed the description

We're actually missing one instance, I think, Timeless.

Oh, wait, we get that because array is not TC opaque. I believe we should make it TC opaque and add that instance explicitly.

PS: Did you do anything else but moving stuff around in this MR?

added 1 commit

• 7810bc37 - comments

Compare with previous version

resolved all threads

Did you do anything else but moving stuff around in this MR?

Yes, I made it TC opaque. ;) I will add a timeless instance.

added 1 commit

• 784e2431 - add timeless instance

Compare with previous version

resolved all threads

merged