diff options
| author |  leino <unknown> | 2015-05-06 17:58:00 -0700 |
|---|---|---|
| committer | leino <unknown> | 2015-05-06 17:58:00 -0700 |
| commit | f98a30f1ad7c441d8ef9e6e5740752723a43413a (patch) | |
| tree | d3be16d38a2de15865b4b25c38b8c07e41ec1173 /Source/Dafny/Cloner.cs | |
| parent | 20f97304dda7dca7259514ca472c3c1b76262013 (diff) | |
Added inductive predicates
Diffstat (limited to 'Source/Dafny/Cloner.cs')
| -rw-r--r-- | Source/Dafny/Cloner.cs | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/Source/Dafny/Cloner.cs b/Source/Dafny/Cloner.cs index 6317e462..1f773365 100644 --- a/Source/Dafny/Cloner.cs +++ b/Source/Dafny/Cloner.cs @@ -604,6 +604,9 @@ namespace Microsoft.Dafny if (f is Predicate) {
return new Predicate(Tok(f.tok), newName, f.HasStaticKeyword, f.IsProtected, f.IsGhost, tps, formals,
req, reads, ens, decreases, body, Predicate.BodyOriginKind.OriginalOrInherited, CloneAttributes(f.Attributes), null);
+ } else if (f is InductivePredicate) {
+ return new InductivePredicate(Tok(f.tok), newName, f.HasStaticKeyword, f.IsProtected, tps, formals,
+ req, reads, ens, body, CloneAttributes(f.Attributes), null);
} else if (f is CoPredicate) {
return new CoPredicate(Tok(f.tok), newName, f.HasStaticKeyword, f.IsProtected, tps, formals,
req, reads, ens, body, CloneAttributes(f.Attributes), null);
|