| Commit message (Collapse) | Author | Age | |
|---|---|---|---|
| * | Compile lambda functions and apply expressions, and change let expr compilation |  Dan Rosén | 2014-08-12 |
| | | |||
| * | Implemented missing routine in runtime system (real-to-int conversion) |  leino | 2014-07-21 |
| | | |||
| * | Compile reals | Rustan Leino | 2014-04-13 |
| | | |||
| * | Merge | Rustan Leino | 2014-01-08 |
| |\ | |||
| * | | Allow left-hand sides of a let expression to be patterns (like in the case ↵ | Rustan Leino | 2014-01-08 |
| | | | | | | | | | | | | | | | of a match expression). Moved the implementation of CondApplyBox, BoxIfNecessary, CondApplyUnbox, and ModeledAsBoxType from class ExpressionTranslator to class Translator. Fixed compilation of match expressions, to allow them anywhere. | ||
| | * | Compile assign-such-that for all integers, not just ones where a bound is found | Rustan Leino | 2014-01-06 |
| |/ | |||
| * | The "choose" statement, hacky and specialized as it was, is now gone. Use ↵ | Rustan Leino | 2013-03-27 |
| | | | | | the assign-such-that statement instead. For example: x :| x in S; | ||
| * | Replaced SuperSetBoundedPool by SubSetBoundedPool, which is much more useful ↵ |  Rustan Leino | 2013-03-27 |
| | | | | | | | in compiling assign-such-that statements Added run-time support for printing sets, multisets, maps, and sequences | ||
| * | Fixed some build/migration issues | Rustan Leino | 2012-10-04 |
 |
index : debian-dafny | |
| Debian packaging for Dafny |
| summaryrefslogtreecommitdiff |