diff options
| author |  Unknown <leino@LEINO6.redmond.corp.microsoft.com> | 2012-05-01 19:03:27 -0700 |
|---|---|---|
| committer | Unknown <leino@LEINO6.redmond.corp.microsoft.com> | 2012-05-01 19:03:27 -0700 |
| commit | 4eac6913448c492602c9ccef20d0ee6d0a7194cc (patch) | |
| tree | c3d442f09edd256723274ac1ce823506dea23494 /Dafny/DafnyAst.cs | |
| parent | 1096701ea6ac332655167e3e849a0df6a7de7b97 (diff) | |
Dafny: improve printing of inductive datatypes
Dafny: don't consider co-datatypes as candidates for default decreases components
Diffstat (limited to 'Dafny/DafnyAst.cs')
| -rw-r--r-- | Dafny/DafnyAst.cs | 15 |
1 files changed, 15 insertions, 0 deletions
diff --git a/Dafny/DafnyAst.cs b/Dafny/DafnyAst.cs index 27f06518..aba2bd92 100644 --- a/Dafny/DafnyAst.cs +++ b/Dafny/DafnyAst.cs @@ -247,6 +247,21 @@ namespace Microsoft.Dafny { }
}
}
+ public bool IsCoDatatype {
+ get {
+ return AsCoDatatype != null;
+ }
+ }
+ public CoDatatypeDecl AsCoDatatype {
+ get {
+ UserDefinedType udt = this as UserDefinedType;
+ if (udt == null) {
+ return null;
+ } else {
+ return udt.ResolvedClass as CoDatatypeDecl;
+ }
+ }
+ }
public bool IsTypeParameter {
get {
UserDefinedType ct = this as UserDefinedType;
|