diff options
Diffstat (limited to 'Source/Dafny/Rewriter.cs')
-rw-r--r-- | Source/Dafny/Rewriter.cs | 6 |
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));
|