1 files changed, 10 insertions, 0 deletions
diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index ae7e1a4c..4a211aee 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -1038,6 +1038,11 @@ namespace Microsoft.Dafny {
       Contract.Requires(1 <= ctors.Count);
       Ctors = ctors;
     }
+    public bool HasFinitePossibleValues {
+      get {
+        return (TypeArgs.Count == 0 && Ctors.TrueForAll(ctr => ctr.Formals.Count == 0));
+      }
+    }
   }
 
   public class IndDatatypeDecl : DatatypeDecl
@@ -3506,6 +3511,11 @@ namespace Microsoft.Dafny {
     public class BoolBoundedPool : BoundedPool
     {
     }
+    public class DatatypeBoundedPool : BoundedPool
+    {
+      public readonly DatatypeDecl Decl;
+      public DatatypeBoundedPool(DatatypeDecl d) { Decl = d; }
+    }
 
     public List<BoundedPool> Bounds;  // initialized and filled in by resolver
     // invariant Bounds == null || Bounds.Count == BoundVars.Count;