Need a way to pattern match datatypes without referencing all nameonly parameters #5907
Labels
kind: enhancement
Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
part: language definition
Relating to the Dafny language definition itself
Part of the motivation for supporting
nameonly
parameters and default arguments was enabling backwards compatibility:However, there's currently no way to deconstruct such datatypes in match statements/expressions that isn't broken when more optional nameonly parameters are added:
(This has been hit in the past in smithy-dafny, when picking up AWS service model changes that should be backwards compatible but aren't because of this)
We need to support syntax similar to
var Foo(a, b, ...) := ...
, or more pessimistically not allow deconstructing datatypes with anynameonly
parameters.The text was updated successfully, but these errors were encountered: