Skip to content

named parameter support when destructureing from the constructor #2319

Open
@seebees

Description

@seebees

given

datatype Foo = Foo(
  nameonly Bar: nat
)

I can var f := Foo( Bar: 5 );
I can also var Foo(b) := f;

I want to be able to use the named parameter.
Something like
var Foo(b := Bar) := f; or var Foo(bar -> b) := f;

Metadata

Metadata

Assignees

No one assigned

    Labels

    difficulty: good-first-issueGood first issueskind: enhancementEnhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafnypart: language definitionRelating to the Dafny language definition itself

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions