summaryrefslogtreecommitdiff
path: root/Source/Dafny/DafnyAst.cs
Commit message (Expand)AuthorAge
* Fix type inference bug in data rank comparison when one side can be a TypeVarGravatar Dan Rosén2014-08-19
* Fix type equality for UserDefinedTypesGravatar Dan Rosén2014-08-15
* Refactor: Change ApplyExpr's Receiver to FunctionGravatar Dan Rosén2014-08-14
* MergeGravatar leino2014-08-13
|\
* | Check for proper use of equality-supporting types also in local variables and...Gravatar leino2014-08-13
| * Addressed CodeContract complaint about purityGravatar Rustan Leino2014-08-12
| * MergeGravatar Dan Rosén2014-08-11
| |\ | |/ |/|
| * Add higher-order-functions and some other goodiesGravatar Dan Rosén2014-08-11
* | MergeGravatar leino2014-08-02
|\ \
* | | Fixed bug Issue 37: expand type synonyms in more (hopefully all) places in th...Gravatar leino2014-08-02
| |/ |/|
| * added trait feature:Gravatar Reza Ahmadi2014-07-18
|/
* Renamed "arbitrary type" to "opaque type"Gravatar Rustan Leino2014-07-15
* Allow an arbitrary-type to take type parametersGravatar Rustan Leino2014-07-15
* Support for type synonyms in refinementsGravatar Rustan Leino2014-07-14
* Added type synonyms. (No support yet for these in refinements.)Gravatar Rustan Leino2014-07-11
* Make reveal axioms from opaque functions quantify over layersGravatar Dan Rosén2014-07-10
* MergeGravatar Rustan Leino2014-07-08
|\
* | Implemented compilation of the int<->real conversions, and changed the resolu...Gravatar Rustan Leino2014-07-08
| * MergeGravatar Dan Rosén2014-07-07
| |\
| * | New logical encoding of types with Is and IsAllocGravatar Dan Rosén2014-07-07
| | * Allow array-type parameters to be filled in automatically.Gravatar leino2014-07-02
| |/ |/|
* | Added tuples and tuple types. Syntax is the expected one, namely parentheses ...Gravatar Rustan Leino2014-06-27
* | Make syntax of "match" expressions and "match" statements the same -- curly b...Gravatar Rustan Leino2014-06-24
* | Invert LHS sub-expressions in forall assignment statements, which gives the o...Gravatar Rustan Leino2014-06-24
| * Fixed issues with absolute file names in the expected output for the lit tests.Gravatar wuestholz2014-06-04
* | Fixed issues with absolute file names in the expected output for the lit tests.Gravatar wuestholz2014-06-04
* | Added support for 'dirty' forall statements.Gravatar chmaria2014-06-03
|/
* Fixed some bugs where various attributes were not properly visited during typ...Gravatar Rustan Leino2014-05-05
* Add support for assumption variables.Gravatar wuestholz2014-04-21
* Members included from different files are now internally marked with an Inclu...Gravatar Rustan Leino2014-04-19
* Allow reals in decreases clausesGravatar Rustan Leino2014-04-08
* MergeGravatar Rustan Leino2014-04-04
|\
* | Also include lower set bounds (bounding a set from below) in witness guesses ...Gravatar Rustan Leino2014-04-04
* | Support the transition from "modify Frame;" to "modify Frame { Body }" by ref...Gravatar Rustan Leino2014-04-04
* | Added "modify Frame { Body }" statement.Gravatar Rustan Leino2014-04-04
* | Added "modify" statement.Gravatar Rustan Leino2014-04-03
| * Basic support for datatype-update syntatic sugarGravatar Bryan Parno2014-04-03
|/
* Auto-set type arguments of built-in collection types, just like for user-defi...Gravatar Rustan Leino2014-03-21
* Fixed resolution bug where "var x := x" was allowed.Gravatar Rustan Leino2014-03-17
* Refactoring: renamed VarDecl to LocalVariable, and renamed VarDeclStmt.Lhss t...Gravatar Rustan Leino2014-03-17
* AST refactoring:Gravatar Rustan Leino2014-03-17
* Added further assistance in coming up with decreases clauses in SCCs with co-...Gravatar Rustan Leino2014-02-24
* Unfinished code -- please forgive (I'm switching machines and will fix shortly)Gravatar Rustan Leino2014-02-24
* Refactored code for dealing with SCCs in the call graph.Gravatar Rustan Leino2014-02-24
* Deprecated "comethod" keyword in favor of "colemma". (Also, "prefix method" -...Gravatar Rustan Leino2014-02-23
* Allow unary minus on realsGravatar Rustan Leino2014-02-13
* Preliminary support for reals in Dafny specs. No compiler suport yet.Gravatar Bryan Parno2014-02-10
* Fixed bug in DafnyExtension (hover text computation would crash if Translator...Gravatar Rustan Leino2014-02-06
* Mark auto-generated expressions (in "decreases" clauses) and don't use these ...Gravatar Rustan Leino2014-02-04
* Produce hover text for many of the refinement omissions (i.e., "..." and the ...Gravatar Rustan Leino2014-01-31