summaryrefslogtreecommitdiff
path: root/Test/dafny0/LetExpr.dfy
Commit message (Expand)AuthorAge
* Fix lit headers implicitly relying on bash-style constructsGravatar Clément Pit--Claudel2015-06-08
* Allow let-such-that expression to be compiled, provided that they provably ha...Gravatar leino2015-03-13
* Language change: All functions and methods declared lexically outside any cla...Gravatar leino2014-12-12
* Set up the same test infrastructure as in Boogie.Gravatar wuestholz2014-05-29
* Allow left-hand sides of a let expression to be patterns (like in the case of...Gravatar Rustan Leino2014-01-08
* Fixed bug with substitutions in let-such-that expressions. This cures Issue 22.Gravatar Rustan Leino2013-07-04
* Renamed "parallel" statement to "forall" statement, and made the parentheses ...Gravatar Rustan Leino2013-03-06
* Dafny: fixed well-formedness checking of LET expressions to allow the RHS to ...Gravatar Rustan Leino2012-02-29
* Dafny: Fixed a bug in the printing of let expressions.Gravatar wuestholz2012-01-24
* Dafny: added let expressions (syntax: "var x := E0; E1")Gravatar Rustan Leino2011-11-14