Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Add the axiom stating that Seq#Take(s, Seq#Length(s)) == s) for all… #4195

Open
wants to merge 2 commits into
base: master
Choose a base branch
from
Open

Add the axiom stating that Seq#Take(s, Seq#Length(s)) == s) for all… #4195

wants to merge 2 commits into from

Commits on Jun 19, 2023

  1. Add the axiom stating that Seq#Take(s, Seq#Length(s)) == s) for all… 

    … sequence `s` (#4194)

A trivial axiom stating `Seq#Take(s, Seq#Length(s)) == s)` for all
sequence `s`. This will help deducing automatically and without using
any workaround that "multiset(arr[..]) == multiset(arr[..arr.Length])"
for any array `arr`.

Fixes #4184

<small>By submitting this pull request, I confirm that my contribution
is made under the terms of the [MIT
license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>
    @btwael
    btwael committed Jun 19, 2023
    Configuration menu
    Copy the full SHA
    862e5f7 View commit details
    Browse the repository at this point in the history

  2. Update Test/git-issues/git-issue-4184.dfy

    @MikaelMayer
    MikaelMayer committed Jun 19, 2023
    Configuration menu
    Copy the full SHA
    68781d8 View commit details
    Browse the repository at this point in the history