diff options
| author | Brian Campbell | 2019-09-19 17:02:50 +0100 |
|---|---|---|
| committer | Brian Campbell | 2019-09-19 17:03:06 +0100 |
| commit | 4bcdbbeff7926b2aac798d0c154ec6fcd64544c4 (patch) | |
| tree | 1cf8a1d1e0ce9245cabde33adbe969263c2694c1 /src | |
| parent | 79f3f95d6b9b589867560ee9be267df5866afadd (diff) | |
Change Coq Hoare logic rules to produce nicer preconditions
In particular, shift state lambdas outside of if/match/let which avoids
unnecessary abstraction/applications. Add more rules to the tactic.
Diffstat (limited to 'src')
0 files changed, 0 insertions, 0 deletions