summaryrefslogtreecommitdiff
path: root/Test/dafny4/NipkowKlein-chapter7.dfy.expect
Commit message (Collapse)AuthorAge
* Improvements to Nipkow and Klein test cases: Changed imap to map, removed ↵Gravatar leino2015-05-29
| | | | need for Total
* Added to the test suite a Dafny encoding of Chapter 7 from the Nipkow and ↵Gravatar leino2015-05-10
Klein book on semantics. It includes many uses of inductive predicates and inductive lemmas.