Closed acruise closed 2 months ago
Hello! This is needed to be able to declare the T
type parameter, which here is necessary because Conc
is invariant in T
.
If we were to make Conc
covariant, we could declare ConcTree.Empty
as a case object
such as here:
https://github.com/epfl-lara/stainless/blob/536d418f47f2699c7f7bc154a8792204714f5cf8/frontends/library/stainless/covcollection/List.scala#L715
Just out of curiosity... :)
https://github.com/epfl-lara/stainless/blob/536d418f47f2699c7f7bc154a8792204714f5cf8/frontends/benchmarks/verification/valid/ConcTree.scala#L82