diff options
| author |  chrishaw <unknown> | 2015-02-26 23:11:11 -0800 |
|---|---|---|
| committer | chrishaw <unknown> | 2015-02-26 23:11:11 -0800 |
| commit | bcb9f9e189461258d9b50aee0565afe3b8c59e5c (patch) | |
| tree | 85914af749444540ef9c6d4b9421c244c3a38116 /Source/Dafny/RefinementTransformer.cs | |
| parent | f9d6586f72af31d7654bf4590f47ac1292348941 (diff) | |
Add imap type, which is like map but may have have infinite size
Diffstat (limited to 'Source/Dafny/RefinementTransformer.cs')
| -rw-r--r-- | Source/Dafny/RefinementTransformer.cs | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/Source/Dafny/RefinementTransformer.cs b/Source/Dafny/RefinementTransformer.cs index 3772d3c0..0ceb56ec 100644 --- a/Source/Dafny/RefinementTransformer.cs +++ b/Source/Dafny/RefinementTransformer.cs @@ -456,7 +456,8 @@ namespace Microsoft.Dafny } else if (prev is MultiSetType) {
return next is MultiSetType && ResolvedTypesAreTheSame(((MultiSetType)prev).Arg, ((MultiSetType)next).Arg);
} else if (prev is MapType) {
- return next is MapType && ResolvedTypesAreTheSame(((MapType)prev).Domain, ((MapType)next).Domain) && ResolvedTypesAreTheSame(((MapType)prev).Range, ((MapType)next).Range);
+ return next is MapType && ((MapType)prev).Finite == ((MapType)next).Finite &&
+ ResolvedTypesAreTheSame(((MapType)prev).Domain, ((MapType)next).Domain) && ResolvedTypesAreTheSame(((MapType)prev).Range, ((MapType)next).Range);
} else if (prev is SeqType) {
return next is SeqType && ResolvedTypesAreTheSame(((SeqType)prev).Arg, ((SeqType)next).Arg);
} else if (prev is UserDefinedType) {
|