diff options
| author |  Unknown <leino@LEINO6.redmond.corp.microsoft.com> | 2012-09-12 16:03:24 -0700 |
|---|---|---|
| committer | Unknown <leino@LEINO6.redmond.corp.microsoft.com> | 2012-09-12 16:03:24 -0700 |
| commit | cd933c5c97b61e04d0d0bd84ad961382e72b57b5 (patch) | |
| tree | 484a572df73b51fee4401f918d9f9bf33825f9b1 /Binaries | |
| parent | fc76541682ec019b8a2dc08ca9972ff517db9b74 (diff) | |
Dafny: things about sequences: parse Suffix expressions after DisplayExpr's, and axiomatize [][..0] == [] == [][0..]
Diffstat (limited to 'Binaries')
| -rw-r--r-- | Binaries/DafnyPrelude.bpl | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl index 53d0b471..ca526173 100644 --- a/Binaries/DafnyPrelude.bpl +++ b/Binaries/DafnyPrelude.bpl @@ -357,6 +357,10 @@ axiom (forall<T> s: Seq T, v: T, n: int :: { Seq#Drop(Seq#Build(s, v), n) }
0 <= n && n <= Seq#Length(s) ==> Seq#Drop(Seq#Build(s, v), n) == Seq#Build(Seq#Drop(s, n), v) );
+// Additional axioms about common things
+axiom Seq#Take(Seq#Empty(): Seq BoxType, 0) == Seq#Empty(); // [][..0] == []
+axiom Seq#Drop(Seq#Empty(): Seq BoxType, 0) == Seq#Empty(); // [][0..] == []
+
// ---------------------------------------------------------------
// -- Axiomatization of Maps -------------------------------------
// ---------------------------------------------------------------
|