summaryrefslogtreecommitdiff
path: root/Test/hofs
Commit message (Expand)AuthorAge
* Revised the $Is and $IsAlloc axioms for arrow terms. It is now possible toGravatar Rustan Leino2016-03-01
* Removed specContextOnly parameter from ResolveStatement.Gravatar leino2015-09-28
* Fix: Unify column numbers in Dafny's errorsGravatar Clément Pit--Claudel2015-07-23
* Type parameters in method/function signatures are no longer auto-declared. A...Gravatar Rustan Leino2015-07-02
* Fixed bugs in encoding of preconditions of function values, Issue #84.Gravatar leino2015-06-30
* Additional test case for instance functionsGravatar leino2015-06-30
* Removed unneeded :heapQuantifier from test case (rendinging this attribute cu...Gravatar leino2015-06-25
* Changed logical order of requires and reads clauses on functions. Reads clausesGravatar Rustan Leino2015-06-15
* Do postponsed reads checking also for the body of functions -- see Test/dafny...Gravatar Rustan Leino2015-06-15
* Postpone reads checks of function preconditions until after the entire precon...Gravatar leino2015-06-15
* Improved generation of .reads axioms (correcting an incorrect answer and corr...Gravatar leino2015-05-01
* Answer fileGravatar leino2015-05-01
* Improved encoding of a property of reads clauses to make things more easily p...Gravatar leino2015-05-01
* Stop pretty-print from emitting deprecated semi-colons.Gravatar qunyanm2015-03-05
* Switched use of List(IToken) in UserDefinedType to NameSegment/ExprDotName, s...Gravatar leino2015-01-23
* Language change: All functions and methods declared lexically outside any cla...Gravatar leino2014-12-12
* Finished up refactoring of the new name segment parsing, AST, and resolution.Gravatar leino2014-12-07
* Snapshot, to be continuedGravatar leino2014-12-02
* Use arbitrary lookahead to determine if the next expression is a lambda expre...Gravatar leino2014-11-13
* Disallow automatic completion of type arguments to the LHS of datatype declar...Gravatar leino2014-10-28
* Print arrow types with parentheses around the domain type when the domain con...Gravatar leino2014-10-09
* Stricter rules about that types need to be completely resolved.Gravatar leino2014-10-08
* Refactored ArrowType's to be resolved with other types. ArrowTypeDecl's are n...Gravatar leino2014-08-27
* Support for non-constrained derived types ("new types").Gravatar leino2014-08-21
* Handle underscores in lambda bound variable lists properlyGravatar Dan Rosén2014-08-19
* Fix type inference bug in data rank comparison when one side can be a TypeVarGravatar Dan Rosén2014-08-19
* Consider lambdas literals + create literal axioms when an argument is a functionGravatar Dan Rosén2014-08-18
* Add Monads as a module example and implementation of some simple monadsGravatar Dan Rosén2014-08-15
* Refactor resolver, and really allow reads to take fields of type A -> set<obj>Gravatar Dan Rosén2014-08-15
* Add the VectorUpdate exampleGravatar Dan Rosén2014-08-14
* Make arrow types not look like reference types for the resolverGravatar Dan Rosén2014-08-14
* Reword error message for type error in lambda requires clauseGravatar Dan Rosén2014-08-14
* Add lambda compilation example, and remove some unused files from the testsGravatar Dan Rosén2014-08-13
* Compile lambda functions and apply expressions, and change let expr compilationGravatar Dan Rosén2014-08-12
* Add higher-order-functions and some other goodiesGravatar Dan Rosén2014-08-11
generated by cgit v1.2.3 (git 2.39.1) at 2024-04-29 15:21:44 +0000