Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Add some minor reflect things | 2019-03-04 | |
| | |||
* | Add zrange_rect{,_Proper,_Proper_dep} | 2019-02-02 | |
| | |||
* | Add a couple of zrange lemmas | 2018-06-26 | |
| | |||
* | Add zrange equality | 2018-06-15 | |
| | |||
* | Add is_bounded_by_None_repeat_In_iff_lt | 2017-06-20 | |
| | |||
* | Add is_bounded_by_None_repeat_In_iff | 2017-06-20 | |
| | |||
* | Fix zrange notation levels | 2017-06-12 | |
| | | | | So that it doesn't interfere with [~> R] and [A ~> B]. | ||
* | More powerful inversion_zrange | 2017-04-15 | |
| | |||
* | Coalesce Tuple.pointwise2 and Tuple.fieldwise | 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 | 2017-03-31 | |
| | |||
* | Use r[_ ~> _] for range rather than b[_ ~> _] | 2017-03-30 | |
| | |||
* | Rename Bounds to ZRange, use Prop, not bool | 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 |