You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
This makes sense as there is currently a single size function per sort.
But this means that the size of a list is just its length, which prevents recursing on its elements.
Could the size of type parameters somehow be taken into account when computing the size of parametric types? That would probably require generating a different size function for each instantiation of a parametric type.
Or are there known workarounds? Defining my own monomorphic list type is one, but it's far from ideal as I have to re-implement and re-prove any method or property I want to use on lists.
The text was updated successfully, but these errors were encountered:
This works:
The same using Stainless'
List
doesn't:which outputs:
I also tried:
which outputs:
I think the problem is that
List
doesn't take the size of its type parameter into account. This is clear when tracingfullSize
:where the
fullSize
of theTypeParameter
T
is0
, that's the default case offullSize
:stainless/core/src/main/scala/stainless/termination/SizeFunctions.scala
Lines 207 to 208 in e5099c5
This makes sense as there is currently a single size function per sort.
But this means that the size of a list is just its length, which prevents recursing on its elements.
Could the size of type parameters somehow be taken into account when computing the size of parametric types? That would probably require generating a different size function for each instantiation of a parametric type.
Or are there known workarounds? Defining my own monomorphic list type is one, but it's far from ideal as I have to re-implement and re-prove any method or property I want to use on lists.
The text was updated successfully, but these errors were encountered: