| Commit message (Expand) | Author | Age |
|---|
| * | Add is_tighter_than_bool to zrange |  Jason Gross | 2017-03-31 |
| * | More compatibility for etransitivity | Jason Gross | 2017-03-31 |
| * | Add [change_with_curried] to Curry.v | Jason Gross | 2017-03-31 |
| * | Add [etransitivity y], [etransitivity_rev] tactics | Jason Gross | 2017-03-31 |
| * | use improved fsatz on various elliptic curve things |  Andres Erbsen | 2017-03-31 |
| * | Add a comment explaining bounds_exp | Jason Gross | 2017-03-30 |
| * | Add wordToZ{_gen,}_range | Jason Gross | 2017-03-30 |
| * | Update IntegrationTest with actual bounds | Jason Gross | 2017-03-30 |
| * | Start instantiating MapCastByDeBruijn in Z/ | Jason Gross | 2017-03-30 |
| * | Created test file for newbasesystem/word-size-selection integration |  jadep | 2017-03-30 |
| * | turn [Let]s into [Definition]s so they persist after the section | jadep | 2017-03-30 |
| * | Reorder arguments to Wf_MapCast for eauto | Jason Gross | 2017-03-30 |
| * | fix a typo | jadep | 2017-03-30 |
| * | change import order to avoid name-clash with [List.repeat] and [Tuple.repeat] | jadep | 2017-03-30 |
| * | Don't linearize and eta in MapCastByDeBruijn | Jason Gross | 2017-03-30 |
| * | Revert "Update CNotations, JavaNotations" | Jason Gross | 2017-03-30 |
| * | rename [Sorted] to [Columns] | jadep | 2017-03-30 |
| * | Proofs for [Sorted.from_associational] | jadep | 2017-03-30 |
| * | create module, indent the things, also rewrite [nils] to use tuple [repeat] a... | jadep | 2017-03-30 |
| * | rewrite zeros to use tuple [repeat] | jadep | 2017-03-30 |
| * | added tuple [repeat] | jadep | 2017-03-30 |
| * | Update CNotations, JavaNotations | Jason Gross | 2017-03-30 |
| * | 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 |
| * | Get rid of list-based Tuple.map | Jason Gross | 2017-03-30 |
| * | Use Bounds in BoundsInterpretations | Jason Gross | 2017-03-30 |
| * | make fsatz recurse when proving nonzero-ness, undo Weierstrass workaround | Andres Erbsen | 2017-03-30 |
| * | Add a file dedicated to the definition of Z bounds | Jason Gross | 2017-03-30 |
| * | Add Tuple.pointwise2, Tuple.map_fix | Jason Gross | 2017-03-30 |
| * | some examples/tests for compact | jadep | 2017-03-29 |
| * | convert compact to CPS and try out a simple example | jadep | 2017-03-29 |
| * | remove commented-out lemma and add CPS version of mapi_with | jadep | 2017-03-29 |
| * | change map_with to mapi_with, a version that handles the index explicitly | jadep | 2017-03-29 |
| * | More robust reifier | Jason Gross | 2017-03-29 |
| * | Add Z.one_succ Z.two_succ to zsimplify_const db | Jason Gross | 2017-03-28 |
| * | Don't reserve '(max_bitwidth' | Jason Gross | 2017-03-28 |
| * | Add a notation for printing | Jason Gross | 2017-03-28 |
| * | Add Z.FoldTypes.{Min,Max}TypeUsed | Jason Gross | 2017-03-28 |
| * | Add FoldTypes | Jason Gross | 2017-03-28 |
| * | Add Wf_MapCast_arrow | Jason Gross | 2017-03-28 |
| * | Add InterpExprEta_arrow | Jason Gross | 2017-03-28 |
| * | Add Wf_MapCast to wf database | Jason Gross | 2017-03-28 |
| * | Break up MapCast into separate pieces for easier debugging | Jason Gross | 2017-03-28 |
| * | Finish proof of wf_map_cast | Jason Gross | 2017-03-28 |
| * | Do more subst in ContextProperties/Tactics | Jason Gross | 2017-03-28 |
| * | Add find_Name_and_val_SmartFlatTypeMapUnInterp2_Some_Some | Jason Gross | 2017-03-28 |
| * | Add SmartVarfMap3 arguments | Jason Gross | 2017-03-28 |
| * | Add SmartVarfMap3 | Jason Gross | 2017-03-28 |
| * | Add Bounds.dec_eq_interp_flat_type | Jason Gross | 2017-03-27 |
| * | Added saturated arithmetic file, including [compact] code and proof | jadep | 2017-03-24 |
Jason Gross
Andres Erbsen
jadep