diff options
| author |  rustanleino <unknown> | 2011-03-04 07:24:29 +0000 |
|---|---|---|
| committer | rustanleino <unknown> | 2011-03-04 07:24:29 +0000 |
| commit | 8a2dd8d4c29df3db73dd13a5457efbee007dfeac (patch) | |
| tree | cb62d829a0da76d3c68c40fbc815a700d2181044 /BCT/BCT.vsmdi | |
| parent | ccc1c910af50b211f66566c981bdb62827d814d6 (diff) | |
Dafny:
* Add support for an {:induction} attribute on universal quantifiers over one bound variable. It causes the universally quantified formulas to be proved by induction.
* For a user-defined function F, introduce not just F and F#limited, but also F#2 (which sits "above" F, just as F sits "above" F#limited)
* In base case of SplitExpr, make use of F#2 functions (unless already inside an inlined predicate)
Diffstat (limited to 'BCT/BCT.vsmdi')
0 files changed, 0 insertions, 0 deletions