| Commit message (Expand) | Author | Age |
|---|
| * | Add commented out proof of equivalence in MxDH |  Jason Gross | 2017-04-12 |
| * | Add denoter for symbolic_expr | Jason Gross | 2017-04-12 |
| * | SOp needs to hold the type of the arguments, for denote | Jason Gross | 2017-04-12 |
| * | Hold types in SFst and SSnd | Jason Gross | 2017-04-12 |
| * | More comment on Saturated.v, explaining representation and the [compact] oper... |  jadep | 2017-04-11 |
| * | More WIP on CSE interp | Jason Gross | 2017-04-11 |
| * | Extend cse context when inlining | Jason Gross | 2017-04-11 |
| * | Add initial version of CSE interp | Jason Gross | 2017-04-11 |
| * | Generalize prepend_prefix | Jason Gross | 2017-04-10 |
| * | Fix missing 'by tac' in rewrite_hyp | Jason Gross | 2017-04-10 |
| * | Finish CSE_Wf | Jason Gross | 2017-04-10 |
| * | Finish most of wf for CSE | Jason Gross | 2017-04-10 |
| * | Reorder parameters for ease of partial instantiation, add symbolic_expr_dec | Jason Gross | 2017-04-10 |
| * | Add dec_of_bool_dec | Jason Gross | 2017-04-10 |
| * | Add lookupb_extendb_full | Jason Gross | 2017-04-10 |
| * | Fix CSE to correctly symbolize expressions | Jason Gross | 2017-04-10 |
| * | Relax extendb, and prove a property about length | Jason Gross | 2017-04-10 |
| * | Key on flat_type not base_type, in CSE | Jason Gross | 2017-04-10 |
| * | Add flatten_binding_list_SmartVarfMap2_pair_In_split | Jason Gross | 2017-04-10 |
| * | Add flatten_binding_list_SmartVarfMap2_pair_same_in_eq2 | Jason Gross | 2017-04-10 |
| * | Use Named.Context in CSE, so we can reuse context lemmas | Jason Gross | 2017-04-10 |
| * | Add AListContext, WeakListContext | Jason Gross | 2017-04-10 |
| * | Split off Compilers.Named.Context | Jason Gross | 2017-04-10 |
| * | Add rewrite_hyp ... by tac | Jason Gross | 2017-04-10 |
| * | Finish the last of the admits in word-size-selection! | Jason Gross | 2017-04-09 |
| * | Split off ZUtil.Stabilization, finish IsBoundedBy! | Jason Gross | 2017-04-09 |
| * | Add Z.lt_le_flip_Proper_flip_impl | Jason Gross | 2017-04-09 |
| * | More wip on bounds | Jason Gross | 2017-04-09 |
| * | Add Z.pow_nonneg to zarith | Jason Gross | 2017-04-09 |
| * | More progress on bounds | Jason Gross | 2017-04-09 |
| * | Don't take abs in upper_lor_and_bounds | Jason Gross | 2017-04-09 |
| * | Make replace_with_neg more powerful | Jason Gross | 2017-04-09 |
| * | Handle more things in Z.peel_le | Jason Gross | 2017-04-09 |
| * | Take more abs in Bounds.Interpretation | Jason Gross | 2017-04-09 |
| * | Add Z.peel_le | Jason Gross | 2017-04-09 |
| * | Factor out Z.{lor,land} proofs a bit more | Jason Gross | 2017-04-09 |
| * | Add Z.log2_up_le_mono to zarith | Jason Gross | 2017-04-09 |
| * | Add Z.max_le_compat Z.min_le_compat to zarith | Jason Gross | 2017-04-09 |
| * | Finish shift cases, extract out land, lor facts | Jason Gross | 2017-04-09 |
| * | Add lemmas about shift bounds to ZUtil | Jason Gross | 2017-04-09 |
| * | Fix missing unfold | Jason Gross | 2017-04-09 |
| * | Add sub_le_flip_le_Proper | Jason Gross | 2017-04-09 |
| * | WIP on bounds lemma | Jason Gross | 2017-04-08 |
| * | Add Z.shift{l,r}_opp_l | Jason Gross | 2017-04-08 |
| * | More WIP on PullCast | Jason Gross | 2017-04-08 |
| * | Add some le proper flip lemmas | Jason Gross | 2017-04-08 |
| * | Add interpToZ_range | Jason Gross | 2017-04-08 |
| * | Add ZToInterp_eq_inj | Jason Gross | 2017-04-08 |
| * | Use Z.max 0, not an if statement | Jason Gross | 2017-04-08 |
| * | Add interpToZ_ZToInterp_mod | Jason Gross | 2017-04-08 |
Jason Gross
jadep