aboutsummaryrefslogtreecommitdiff
path: root/src/Compilers/Z/Bounds/InterpretationLemmas/IsBoundedBy.v
Commit message (Expand)AuthorAge
* Add Z.land, Z.lor bounds stuff to zutil, also split up ZUtilGravatar Jason Gross2018-08-23
* Try out stronger land, lor boundsGravatar Jason Gross2018-06-27
* Split off ZRange lemmasGravatar Jason Gross2018-02-10
* Fix a spelling errorGravatar Jason Gross2017-10-13
* Factor out truncation_boundsGravatar Jason Gross2017-10-13
* Unfold Z.mul_split_at_bitwidth for reificationGravatar Jason Gross2017-06-17
* Reify Z.mul_with_split_at_bitwidthGravatar Jason Gross2017-06-13
* Push bounds side conditions through the pipelineGravatar Jason Gross2017-06-12
* Initial stab at id_with_altGravatar Jason Gross2017-06-11
* Add dummy version of IdWithAlt to compilersGravatar Jason Gross2017-06-11
* Add SubWithGetBorrow to reflective machineryGravatar Jason Gross2017-05-20
* Add reflective machinery for adc, zselectGravatar Jason Gross2017-05-17
* Split off ZUtil.Stabilization, finish IsBoundedBy!Gravatar Jason Gross2017-04-09
* More wip on boundsGravatar Jason Gross2017-04-09
* More progress on boundsGravatar Jason Gross2017-04-09
* Factor out Z.{lor,land} proofs a bit moreGravatar Jason Gross2017-04-09
* Finish shift cases, extract out land, lor factsGravatar Jason Gross2017-04-09
* WIP on bounds lemmaGravatar Jason Gross2017-04-08
* Split up Compilers/Z/Bounds/InterpretationLemmasGravatar Jason Gross2017-04-07
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-27 05:27:27 +0000