summaryrefslogtreecommitdiff
path: root/lib/coq/Sail2_state_lemmas.v
AgeCommit message (Expand)Author
2020-06-10Prepare Coq library for packagingBrian Campbell
2019-12-19Coq library improvementsBrian Campbell
2019-12-06Coq: use proof irrelevance for a few propertiesBrian Campbell
2019-11-29Coq: switch to boolean predicates for Sail-type propertiesBrian Campbell
2019-11-13Coq: more proof supportBrian Campbell
2019-10-24Coq: use `abstract` to separate out proofs from definitionsBrian Campbell
2019-10-18Coq: tweak a state monad lifting rule to improve performanceBrian Campbell
2019-09-19Expand Coq Hoare logic and congruence rules to more operatorsBrian Campbell
2019-08-22Coq: tactics to do rewrites under state monad, simple wp computationBrian Campbell
2019-08-19Coq: add bools_of_bits_nondet and friends to libraryBrian Campbell
2019-08-14Coq library work for proofs:Brian Campbell
2019-07-31Coq: reasoning for until loopsBrian Campbell
2019-07-29Coq: add state monad version of while/until loops and lifting resultsBrian Campbell
2019-07-25Basic port of proof machinery to CoqBrian Campbell
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 03:31:11 +0000