We can presumably extract erased parameter keyword and map it to Stainless @ghost.
First, introduce ErasedChecks that has require, ensuring, assert, etc. all expecting erased parameters.
We need to keep StaticChecks for legacy reasons.
We should start by writing some code that uses erased instead of ghost and compiles with Scala 3 (even without Stainless).
There are differences between erased, including the fact that var-s are possibly not marked by erased. Still, being able to remove immutable parameters of defs and case classes is already useful, as it allows to not rely on our own ghost code elimination.
Scala 3 has erased definitions: https://dotty.epfl.ch/docs/reference/experimental/erased-defs.html
We can presumably extract
erasedparameter keyword and map it to Stainless@ghost.First, introduce ErasedChecks that has require, ensuring, assert, etc. all expecting
erasedparameters. We need to keep StaticChecks for legacy reasons.We should start by writing some code that uses erased instead of ghost and compiles with Scala 3 (even without Stainless).
There are differences between erased, including the fact that
var-s are possibly not marked byerased. Still, being able to remove immutable parameters ofdefs and case classes is already useful, as it allows to not rely on our own ghost code elimination.