diff options
| author | Brian Campbell | 2019-11-13 18:05:23 +0000 |
|---|---|---|
| committer | Brian Campbell | 2019-11-13 18:05:53 +0000 |
| commit | b141285b7f2a07dd845463922788195d25071bd1 (patch) | |
| tree | c1bf934894c50e6c6bd1d490082ef9f24d61f6ed /src/spec_analysis.ml | |
| parent | cd49c9df8e1d688327ae045729b538df00b77622 (diff) | |
Coq: more proof support
- add state versions of foreach combinators
- support dependent sumbool pattern matching (i.e., those where the
property is actually used)
- add rewriting congruence rules, state monad lifting rules,
and invariant proof rules for these
Diffstat (limited to 'src/spec_analysis.ml')
0 files changed, 0 insertions, 0 deletions