Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Add some minor reflect things | Jason Gross | 2019-03-04 |
| | |||
* | Add zrange_rect{,_Proper,_Proper_dep} | Jason Gross | 2019-02-02 |
| | |||
* | Add a couple of zrange lemmas | Jason Gross | 2018-06-26 |
| | |||
* | Add zrange equality | Jason Gross | 2018-06-15 |
| | |||
* | Add is_bounded_by_None_repeat_In_iff_lt | Jason Gross | 2017-06-20 |
| | |||
* | Add is_bounded_by_None_repeat_In_iff | Jason Gross | 2017-06-20 |
| | |||
* | Fix zrange notation levels | Jason Gross | 2017-06-12 |
| | | | | So that it doesn't interfere with [~> R] and [A ~> B]. | ||
* | More powerful inversion_zrange | Jason Gross | 2017-04-15 |
| | |||
* | Coalesce Tuple.pointwise2 and Tuple.fieldwise | Jason Gross | 2017-04-02 |
| | | | | | | We don't need both of them. We keep the definition of pointwise2 because it's needed for reification to work, and we keep the name of fieldwise because it's used in more places. This closes #137. | ||
* | Add is_tighter_than_bool to zrange | Jason Gross | 2017-03-31 |
| | |||
* | Use r[_ ~> _] for range rather than b[_ ~> _] | Jason Gross | 2017-03-30 |
| | |||
* | Rename Bounds to ZRange, use Prop, not bool | Jason Gross | 2017-03-30 |
As per @andres-erbsen's comments at https://github.com/mit-plv/fiat-crypto/commit/ba864554da71ebe20b2494b1e8adf04779cd904b#commitcomment-21565223, https://github.com/mit-plv/fiat-crypto/commit/ba864554da71ebe20b2494b1e8adf04779cd904b#commitcomment-21565200 |