dafny-lang / libraries

Libraries useful for Dafny programs
Other
43 stars 25 forks source link

feat: Functional constructs for methods #29

Open seebees opened 2 years ago

seebees commented 2 years ago

Being able to express logic with map and filter simplifies the expression of an implementation.

However doing this iteration in a method requires a loop. Loop invariants are hard.

@robin-aws here is the implementation we have been talking about. Obviously we need examples before we could merge, but this can start a discussion about if/how such constructs could be used or simplified.