Open stefan-aws opened 1 year ago
Why does it need to be in a separate module, as opposed to adding more of the functions above to the existing version in Wrappers
?
There are so many standard wrappers/monads, each with numerous functions, that this approach won't scale, in my opinion. (I will suggest more examples in other issues.) For readability, I'd create one file each. This is also how it is done in Ocaml (https://github.com/ocaml/ocaml/tree/trunk/stdlib). We'll have even more code, as we also provide lemmas.
I suggest we move the relevant code in https://github.com/dafny-lang/libraries/blob/master/src/Wrappers.dfy to a separate module that contains a superset of the code below. I am following https://github.com/ocaml/ocaml/blob/trunk/stdlib/option.ml.