diff options
| author |  Rustan Leino <unknown> | 2015-10-02 15:26:56 -0700 |
|---|---|---|
| committer | Rustan Leino <unknown> | 2015-10-02 15:26:56 -0700 |
| commit | 1885f7d7d1fb9bd6ceb8220450dbb5d890501337 (patch) | |
| tree | d85a7c88c668f883aadda5bb5412fe15f3bd5102 /Test/dafny4/NipkowKlein-chapter7.dfy | |
| parent | c5a1c58d3c89c55c31331cb419cd3c06e276b5dd (diff) | |
Hover text includes #[_k-1] suffix for terms rewritten in prefix predicates/lemmas (this fixes an item from the wishlist).
Include in hover text the extreme predicates for which an extreme lemmas has been rewritten (but don't include ==# in this list--or should it perhaps be included?).
Under a (temporary) switch /rewriteFocalPredicates, each use of a focal predicate P in a prefix lemma is rewritten into P#[_k-1].
Diffstat (limited to 'Test/dafny4/NipkowKlein-chapter7.dfy')
0 files changed, 0 insertions, 0 deletions