diff options
| author | Brian Campbell | 2019-11-29 15:09:17 +0000 |
|---|---|---|
| committer | Brian Campbell | 2019-11-29 15:09:17 +0000 |
| commit | aeba539412d37f4e0f6b8e02bea7389b433fbb80 (patch) | |
| tree | c1f87482e219bf0b8c2d2e87604aebb977b6ad0c /x86 | |
| parent | beebcc35f79e2e30fe029f9b88ffd355f1276ec9 (diff) | |
Coq: switch to boolean predicates for Sail-type properties
- ArithFact takes a boolean predicate
- defined in terms of ArithFactP, which takes a Prop predicate,
and is used directly for existentials
- used abstract in more definitions with direct proofs
- beef up solve_bool_with_Z to handle more equalities, andb and orb
Diffstat (limited to 'x86')
0 files changed, 0 insertions, 0 deletions