aboutsummaryrefslogtreecommitdiff
path: root/src/Compilers/Z/Bounds/InterpretationLemmas/PullCast.v
Commit message (Expand)AuthorAge
* Add reflective machinery for adc, zselectGravatar Jason Gross2017-05-17
* Finish the last of the admits in word-size-selection!Gravatar Jason Gross2017-04-09
* More WIP on PullCastGravatar Jason Gross2017-04-08
* More WIP on PullCastGravatar Jason Gross2017-04-08
* WIP on pullcastGravatar Jason Gross2017-04-08
* Work in progress on proving PullCastGravatar Jason Gross2017-04-07
* Split up Compilers/Z/Bounds/InterpretationLemmasGravatar Jason Gross2017-04-07