Unique Maximum Element - Githubissues

dafny-lang / libraries

Libraries useful for Dafny programs

Other

43 stars 25 forks source link

Closed stefan-aws closed 1 year ago

stefan-aws commented 1 year ago

Per request, adds the lemma LemmaUniqueMaximum, which is analogous to the existing one LemmaUniqueMinimum
Per request, moves both lemmas from Relations.dfy to Sets.dfy (both for existing library and new/dafny subfolder)

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

stefan-aws commented 1 year ago

Still copying code in this PR, but will only commit to src/dafny in the future.

stefan-aws commented 1 year ago

Thanks for the hints, I added additional material and now distinguish between:

and