Fixed bug Issue 37: expand type synonyms in more (hopefully all) places in the resolver and translator

1 files changed, 3 insertions, 3 deletions

diff --git a/Source/Dafny/Rewriter.cs b/Source/Dafny/Rewriter.cs
index ca3c105d..63bb2dcc 100644
--- a/Source/Dafny/Rewriter.cs
+++ b/Source/Dafny/Rewriter.cs
@@ -174,7 +174,7 @@ namespace Microsoft.Dafny
           }

         } else if (member is Function && member.Name == "Valid" && !member.IsStatic) {

           var fn = (Function)member;

-          if (fn.Formals.Count == 0 && fn.ResultType is BoolType) {

+          if (fn.Formals.Count == 0 && fn.ResultType.IsBoolType) {

             Valid = fn;

           }

         }

@@ -201,7 +201,7 @@ namespace Microsoft.Dafny
         Boogie.IToken tok = new AutoGeneratedToken(member.tok);

         if (member is Function && member.Name == "Valid" && !member.IsStatic) {

           var valid = (Function)member;

-          if (valid.IsGhost && valid.ResultType is BoolType) {

+          if (valid.IsGhost && valid.ResultType.IsBoolType) {

             Expression c;

             if (valid.RefinementBase == null) {

               var c0 = BinBoolExpr(tok, BinaryExpr.ResolvedOpcode.InSet, self, Repr);  // this in Repr

@@ -265,7 +265,7 @@ namespace Microsoft.Dafny
               var valid = new FunctionCallExpr(tok, "Valid", implicitSelf, tok, new List<Expression>());

               valid.Function = Valid;

               valid.Type = Type.Bool;

-							// Add the identity substitution to this call

+              // Add the identity substitution to this call

               valid.TypeArgumentSubstitutions = new Dictionary<TypeParameter, Type>();

               foreach (var p in cl.TypeArgs) {

                 valid.TypeArgumentSubstitutions.Add(p, new UserDefinedType(p));