Allow left-hand sides of a let expression to be patterns (like in the case of a match expression).

Moved the implementation of CondApplyBox, BoxIfNecessary, CondApplyUnbox, and ModeledAsBoxType from class ExpressionTranslator to class Translator.
Fixed compilation of match expressions, to allow them anywhere.

1 files changed, 1 insertions, 0 deletions

diff --git a/Binaries/DafnyRuntime.cs b/Binaries/DafnyRuntime.cs
index a8faafae..3afac587 100644
--- a/Binaries/DafnyRuntime.cs
+++ b/Binaries/DafnyRuntime.cs
@@ -627,5 +627,6 @@ namespace Dafny
     {

       return u;

     }

+    public delegate Result Function<Input,Result>(Input input);

   }

 }