diff options
| author |  Bryan Parno <parno@microsoft.com> | 2014-02-10 16:48:43 -0800 |
|---|---|---|
| committer | Bryan Parno <parno@microsoft.com> | 2014-02-10 16:48:43 -0800 |
| commit | f0f4e3acbabc7386dafce96ea6b077896045bb73 (patch) | |
| tree | 84e8646b4e9bea0506473cb609b737fe94ff5d52 /Source/Dafny/RefinementTransformer.cs | |
| parent | 783c272bb035c7ce419c312cd7ade5a8de378d75 (diff) | |
Preliminary support for reals in Dafny specs. No compiler suport yet.
Diffstat (limited to 'Source/Dafny/RefinementTransformer.cs')
| -rw-r--r-- | Source/Dafny/RefinementTransformer.cs | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/Source/Dafny/RefinementTransformer.cs b/Source/Dafny/RefinementTransformer.cs index 345c5fbb..acee1845 100644 --- a/Source/Dafny/RefinementTransformer.cs +++ b/Source/Dafny/RefinementTransformer.cs @@ -438,6 +438,8 @@ namespace Microsoft.Dafny if (next is IntType) {
return (prev is NatType) == (next is NatType);
} else return false;
+ } else if (prev is RealType) {
+ return next is RealType;
} else if (prev is ObjectType) {
return next is ObjectType;
} else if (prev is SetType) {
|