summaryrefslogtreecommitdiff
path: root/lib/coq/Sail2_state.v
AgeCommit message (Expand)Author
2020-06-10Prepare Coq library for packagingBrian 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-09-19Expand Coq Hoare logic and congruence rules to more operatorsBrian 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
2019-04-10Coq: update prompt monad to match the Lem, and port the state monad/liftingBrian Campbell
2018-06-22Coq: library updates, esp extending bitvector multiplies, UndefinedBrian Campbell
2018-06-19Coq: library name update (as we did for Lem)Brian Campbell
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 10:45:15 +0000