diff options
| author |  Rustan Leino <leino@microsoft.com> | 2012-01-04 13:15:58 -0800 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2012-01-04 13:15:58 -0800 |
| commit | 30fa66eb8f848eb1549c0335728c4f2790f73b72 (patch) | |
| tree | f235cb9e7c2954b2b94012d9b2f59dedcc28677a /Binaries | |
| parent | 44f63e63bced20568ba2a97f143304e6c64c3f46 (diff) | |
Dafny: compile let expressions efficiently (i.e., with an extra variable, not with a substitution)
Diffstat (limited to 'Binaries')
| -rw-r--r-- | Binaries/DafnyRuntime.cs | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/Binaries/DafnyRuntime.cs b/Binaries/DafnyRuntime.cs index e22d52ad..36341f68 100644 --- a/Binaries/DafnyRuntime.cs +++ b/Binaries/DafnyRuntime.cs @@ -455,5 +455,9 @@ namespace Dafny public static Sequence<T> SeqFromArray<T>(T[] array) {
return new Sequence<T>(array);
}
+ public static U ExpressionSequence<T, U>(T t, U u)
+ {
+ return u;
+ }
}
}
|