diff options
author | 2011-04-19 16:48:32 -0700 | |
---|---|---|
committer | 2011-04-19 16:48:32 -0700 | |
commit | 5bd736fee46b289c130110fdf5cad91aa97d9475 (patch) | |
tree | 63b4a5162863c8bad084b9d1163eaa1a126f2dde /Source/Dafny/DafnyAst.cs | |
parent | 2ebe4385e9146fb1ba568fb2a8ad5d8475303cc8 (diff) |
Dafny: added type "nat"
Diffstat (limited to 'Source/Dafny/DafnyAst.cs')
-rw-r--r-- | Source/Dafny/DafnyAst.cs | 20 |
1 files changed, 16 insertions, 4 deletions
diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs index 045f879a..69756d76 100644 --- a/Source/Dafny/DafnyAst.cs +++ b/Source/Dafny/DafnyAst.cs @@ -135,6 +135,10 @@ namespace Microsoft.Dafny { }
}
+ public bool IsSubrangeType {
+ get { return this is NatType; }
+ }
+
public bool IsRefType {
get {
if (this is ObjectType) {
@@ -197,7 +201,16 @@ namespace Microsoft.Dafny { }
}
- public class ObjectType : BasicType {
+ public class NatType : IntType
+ {
+ [Pure]
+ public override string ToString() {
+ return "nat";
+ }
+ }
+
+ public class ObjectType : BasicType
+ {
[Pure]
public override string ToString() {
return "object";
@@ -218,9 +231,8 @@ namespace Microsoft.Dafny { }
public class SetType : CollectionType {
- public SetType(Type arg) :base(arg){
+ public SetType(Type arg) : base(arg) {
Contract.Requires(arg != null);
-
}
[Pure]
public override string ToString() {
@@ -231,7 +243,7 @@ namespace Microsoft.Dafny { }
public class SeqType : CollectionType {
- public SeqType(Type arg):base(arg) {
+ public SeqType(Type arg) : base(arg) {
Contract.Requires(arg != null);
}
|