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
In Partitions.thy, the documentations of definition coarser_partitions_with and definition coarser_partitions_with_list currently assume that the argument P is a partition. In practice P will be a partition but we can't be sure of that. We should also prove that, when P is a partition, coarser_partitions_with behaves as expected. (OK, actually it does, as certified by the overall equivalence proof for all_partitions*.)
The text was updated successfully, but these errors were encountered:
In Partitions.thy, the documentations of
definition coarser_partitions_with
anddefinition coarser_partitions_with_list
currently assume that the argumentP
is a partition. In practiceP
will be a partition but we can't be sure of that. We should also prove that, whenP
is a partition,coarser_partitions_with
behaves as expected. (OK, actually it does, as certified by the overall equivalence proof forall_partitions*
.)The text was updated successfully, but these errors were encountered: