| Commit message (Expand) | Author | Age |
|---|
| ... | |
| * | 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 |
| * | make update-_CoqProject | 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 |
| * | crypto-defects.md: add two tweetnacl bugs | Andres Erbsen | 2017-03-26 |
| * | Added saturated arithmetic file, including [compact] code and proof | jadep | 2017-03-24 |
| * | Add lemmas needed for saturated arithmetic [compact] | jadep | 2017-03-24 |
| * | Fix binder counting in MapCastByDB | Jason Gross | 2017-03-22 |
| * | Add aborted CompileProperties | Jason Gross | 2017-03-22 |
| * | Add split_onames_split_names | Jason Gross | 2017-03-22 |
| * | Add length_fst_split_names_None_iff | Jason Gross | 2017-03-22 |
| * | Also count lets in operations and pairs | Jason Gross | 2017-03-22 |
| * | Add length_fst_split_names_Some_iff | Jason Gross | 2017-03-22 |
jadep
Jason Gross
Andres Erbsen