diff options
| author |  leino <unknown> | 2015-05-07 08:55:44 -0700 |
|---|---|---|
| committer | leino <unknown> | 2015-05-07 08:55:44 -0700 |
| commit | cafbf508ea7aa6f337140293105060393ccb11f5 (patch) | |
| tree | 5885eeda1ea285e3b043da8ffa8d7633d0a6fc0d /Source/Dafny/RefinementTransformer.cs | |
| parent | f98a30f1ad7c441d8ef9e6e5740752723a43413a (diff) | |
Added "inductive lemma" methods
Diffstat (limited to 'Source/Dafny/RefinementTransformer.cs')
| -rw-r--r-- | Source/Dafny/RefinementTransformer.cs | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/Source/Dafny/RefinementTransformer.cs b/Source/Dafny/RefinementTransformer.cs index 1bdc1265..d819652d 100644 --- a/Source/Dafny/RefinementTransformer.cs +++ b/Source/Dafny/RefinementTransformer.cs @@ -579,6 +579,9 @@ namespace Microsoft.Dafny if (m is Constructor) {
return new Constructor(new RefinementToken(m.tok, moduleUnderConstruction), m.Name, tps, ins,
req, mod, ens, decreases, body, refinementCloner.MergeAttributes(m.Attributes, moreAttributes), null);
+ } else if (m is InductiveLemma) {
+ return new InductiveLemma(new RefinementToken(m.tok, moduleUnderConstruction), m.Name, m.HasStaticKeyword, tps, ins, m.Outs.ConvertAll(refinementCloner.CloneFormal),
+ req, mod, ens, decreases, body, refinementCloner.MergeAttributes(m.Attributes, moreAttributes), null);
} else if (m is CoLemma) {
return new CoLemma(new RefinementToken(m.tok, moduleUnderConstruction), m.Name, m.HasStaticKeyword, tps, ins, m.Outs.ConvertAll(refinementCloner.CloneFormal),
req, mod, ens, decreases, body, refinementCloner.MergeAttributes(m.Attributes, moreAttributes), null);
|