summaryrefslogtreecommitdiff
path: root/Test/dafny1/Induction.dfy
Commit message (Expand)AuthorAge
* Implement workarounds for some tests that fail with /autoTriggers.Gravatar Clément Pit--Claudel2015-08-28
* Renamed "ghost method" to "lemma" in a couple of test filesGravatar Rustan Leino2015-07-24
* Stop pretty-print from emitting deprecated semi-colons.Gravatar qunyanm2015-03-05
* Set up the same test infrastructure as in Boogie.Gravatar wuestholz2014-05-29
* Dafny induction:Gravatar Rustan Leino2011-10-29
* MergeGravatar Rustan Leino2011-05-27
|\
| * Dafny: permanently changed the syntax of "datatype" declarations to what prev...Gravatar Rustan Leino2011-05-27
* | Dafny: fixed bug in induction-tactic heuristic (should never pick values whos...Gravatar Rustan Leino2011-05-26
| * Dafny: retired the "call" keywordGravatar Rustan Leino2011-05-26
| * Dafny:Gravatar Rustan Leino2011-05-21
|/
* Dafny: Alternative (and candidate replacement) syntax for declaring datatypesGravatar Rustan Leino2011-04-20
* Dafny: fixed bug in induction over integersGravatar Unknown2011-04-04
* Dafny: compile quantifiersGravatar rustanleino2011-03-26
* Dafny: Added heuristic for when to turn on the induction tacticGravatar rustanleino2011-03-05
* Dafny:Gravatar rustanleino2011-03-04
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-15 23:31:08 +0000